(set-logic QF_LRA)
(set-info :source |
Formulas from temporal metric planning problems contributed by Jiae Shin.  See
http://cs.nyu.edu/~jiae.

This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun b14 () Bool)
(declare-fun b20 () Bool)
(declare-fun b26 () Bool)
(declare-fun b32 () Bool)
(declare-fun b40 () Bool)
(declare-fun b46 () Bool)
(declare-fun b51 () Bool)
(declare-fun b56 () Bool)
(declare-fun b62 () Bool)
(declare-fun b67 () Bool)
(declare-fun b72 () Bool)
(declare-fun b78 () Bool)
(declare-fun b83 () Bool)
(declare-fun b89 () Bool)
(declare-fun b95 () Bool)
(declare-fun b101 () Bool)
(declare-fun b105 () Bool)
(declare-fun b109 () Bool)
(declare-fun b113 () Bool)
(declare-fun b118 () Bool)
(declare-fun b122 () Bool)
(declare-fun b126 () Bool)
(declare-fun b131 () Bool)
(declare-fun b136 () Bool)
(declare-fun b141 () Bool)
(declare-fun b146 () Bool)
(declare-fun b151 () Bool)
(declare-fun b156 () Bool)
(declare-fun b161 () Bool)
(declare-fun b166 () Bool)
(declare-fun b170 () Bool)
(declare-fun b174 () Bool)
(declare-fun b177 () Bool)
(declare-fun b180 () Bool)
(declare-fun b183 () Bool)
(declare-fun b186 () Bool)
(declare-fun b189 () Bool)
(declare-fun b192 () Bool)
(declare-fun b195 () Bool)
(declare-fun b198 () Bool)
(declare-fun b202 () Bool)
(declare-fun b205 () Bool)
(declare-fun b208 () Bool)
(declare-fun b211 () Bool)
(declare-fun b214 () Bool)
(declare-fun b217 () Bool)
(declare-fun b220 () Bool)
(declare-fun b223 () Bool)
(declare-fun b226 () Bool)
(declare-fun b229 () Bool)
(declare-fun b232 () Bool)
(declare-fun b235 () Bool)
(declare-fun b238 () Bool)
(declare-fun b241 () Bool)
(declare-fun b244 () Bool)
(declare-fun b247 () Bool)
(declare-fun b250 () Bool)
(declare-fun b253 () Bool)
(declare-fun b256 () Bool)
(declare-fun b259 () Bool)
(declare-fun b262 () Bool)
(declare-fun b265 () Bool)
(declare-fun b268 () Bool)
(declare-fun b271 () Bool)
(declare-fun b274 () Bool)
(declare-fun b277 () Bool)
(declare-fun b280 () Bool)
(declare-fun b283 () Bool)
(declare-fun b289 () Bool)
(declare-fun b295 () Bool)
(declare-fun b301 () Bool)
(declare-fun b310 () Bool)
(declare-fun b316 () Bool)
(declare-fun b322 () Bool)
(declare-fun b328 () Bool)
(declare-fun b337 () Bool)
(declare-fun b342 () Bool)
(declare-fun b347 () Bool)
(declare-fun b352 () Bool)
(declare-fun b357 () Bool)
(declare-fun b363 () Bool)
(declare-fun b369 () Bool)
(declare-fun b375 () Bool)
(declare-fun b381 () Bool)
(declare-fun b387 () Bool)
(declare-fun b393 () Bool)
(declare-fun b400 () Bool)
(declare-fun b405 () Bool)
(declare-fun b410 () Bool)
(declare-fun b415 () Bool)
(declare-fun b420 () Bool)
(declare-fun b426 () Bool)
(declare-fun b432 () Bool)
(declare-fun b437 () Bool)
(declare-fun b442 () Bool)
(declare-fun b447 () Bool)
(declare-fun b452 () Bool)
(declare-fun b457 () Bool)
(declare-fun b464 () Bool)
(declare-fun b471 () Bool)
(declare-fun b478 () Bool)
(declare-fun b487 () Bool)
(declare-fun b493 () Bool)
(declare-fun b499 () Bool)
(declare-fun b505 () Bool)
(declare-fun b513 () Bool)
(declare-fun b518 () Bool)
(declare-fun b523 () Bool)
(declare-fun b528 () Bool)
(declare-fun b533 () Bool)
(declare-fun b540 () Bool)
(declare-fun b546 () Bool)
(declare-fun b552 () Bool)
(declare-fun b558 () Bool)
(declare-fun b564 () Bool)
(declare-fun b570 () Bool)
(declare-fun b577 () Bool)
(declare-fun b582 () Bool)
(declare-fun b587 () Bool)
(declare-fun b592 () Bool)
(declare-fun b597 () Bool)
(declare-fun b603 () Bool)
(declare-fun b609 () Bool)
(declare-fun b614 () Bool)
(declare-fun b619 () Bool)
(declare-fun b624 () Bool)
(declare-fun b629 () Bool)
(declare-fun b633 () Bool)
(declare-fun b636 () Bool)
(declare-fun b639 () Bool)
(declare-fun b642 () Bool)
(declare-fun b645 () Bool)
(declare-fun b648 () Bool)
(declare-fun b649 () Bool)
(declare-fun b650 () Bool)
(declare-fun b651 () Bool)
(declare-fun b652 () Bool)
(declare-fun b653 () Bool)
(declare-fun b656 () Bool)
(declare-fun b657 () Bool)
(declare-fun b658 () Bool)
(declare-fun b659 () Bool)
(declare-fun b660 () Bool)
(declare-fun b16 () Bool)
(declare-fun b17 () Bool)
(declare-fun b18 () Bool)
(declare-fun b22 () Bool)
(declare-fun b23 () Bool)
(declare-fun b24 () Bool)
(declare-fun b28 () Bool)
(declare-fun b29 () Bool)
(declare-fun b30 () Bool)
(declare-fun b34 () Bool)
(declare-fun b35 () Bool)
(declare-fun b36 () Bool)
(declare-fun b38 () Bool)
(declare-fun b42 () Bool)
(declare-fun b43 () Bool)
(declare-fun b44 () Bool)
(declare-fun b48 () Bool)
(declare-fun b49 () Bool)
(declare-fun b53 () Bool)
(declare-fun b54 () Bool)
(declare-fun b58 () Bool)
(declare-fun b59 () Bool)
(declare-fun b60 () Bool)
(declare-fun b64 () Bool)
(declare-fun b65 () Bool)
(declare-fun b69 () Bool)
(declare-fun b70 () Bool)
(declare-fun b74 () Bool)
(declare-fun b75 () Bool)
(declare-fun b76 () Bool)
(declare-fun b80 () Bool)
(declare-fun b81 () Bool)
(declare-fun b85 () Bool)
(declare-fun b86 () Bool)
(declare-fun b87 () Bool)
(declare-fun b91 () Bool)
(declare-fun b92 () Bool)
(declare-fun b93 () Bool)
(declare-fun b97 () Bool)
(declare-fun b98 () Bool)
(declare-fun b99 () Bool)
(declare-fun b103 () Bool)
(declare-fun b107 () Bool)
(declare-fun b111 () Bool)
(declare-fun b115 () Bool)
(declare-fun b116 () Bool)
(declare-fun b120 () Bool)
(declare-fun b124 () Bool)
(declare-fun b128 () Bool)
(declare-fun b129 () Bool)
(declare-fun b133 () Bool)
(declare-fun b134 () Bool)
(declare-fun b138 () Bool)
(declare-fun b139 () Bool)
(declare-fun b143 () Bool)
(declare-fun b144 () Bool)
(declare-fun b148 () Bool)
(declare-fun b149 () Bool)
(declare-fun b153 () Bool)
(declare-fun b154 () Bool)
(declare-fun b158 () Bool)
(declare-fun b163 () Bool)
(declare-fun b164 () Bool)
(declare-fun b168 () Bool)
(declare-fun b172 () Bool)
(declare-fun b200 () Bool)
(declare-fun b308 () Bool)
(declare-fun b335 () Bool)
(declare-fun b397 () Bool)
(declare-fun r1 () Real)
(declare-fun r2 () Real)
(declare-fun r3 () Real)
(declare-fun r4 () Real)
(declare-fun r5 () Real)
(declare-fun r6 () Real)
(declare-fun r7 () Real)
(declare-fun r8 () Real)
(declare-fun r9 () Real)
(declare-fun r10 () Real)
(declare-fun r11 () Real)
(declare-fun r12 () Real)
(declare-fun r13 () Real)
(declare-fun r14 () Real)
(declare-fun r15 () Real)
(declare-fun r16 () Real)
(declare-fun r17 () Real)
(declare-fun r18 () Real)
(declare-fun r19 () Real)
(declare-fun r20 () Real)
(declare-fun r21 () Real)
(declare-fun r22 () Real)
(declare-fun r23 () Real)
(declare-fun r24 () Real)
(declare-fun r25 () Real)
(declare-fun r26 () Real)
(declare-fun r27 () Real)
(declare-fun r28 () Real)
(declare-fun r29 () Real)
(declare-fun r30 () Real)
(declare-fun r31 () Real)
(declare-fun r32 () Real)
(declare-fun r33 () Real)
(declare-fun r34 () Real)
(declare-fun r35 () Real)
(declare-fun r36 () Real)
(declare-fun r37 () Real)
(declare-fun r38 () Real)
(declare-fun r39 () Real)
(declare-fun r40 () Real)
(declare-fun r41 () Real)
(declare-fun r42 () Real)
(declare-fun r43 () Real)
(declare-fun r44 () Real)
(declare-fun r45 () Real)
(declare-fun r46 () Real)
(declare-fun r47 () Real)
(declare-fun r48 () Real)
(declare-fun r49 () Real)
(declare-fun r50 () Real)
(declare-fun r51 () Real)
(declare-fun r52 () Real)
(declare-fun r53 () Real)
(declare-fun r54 () Real)
(declare-fun r55 () Real)
(declare-fun r56 () Real)
(declare-fun r57 () Real)
(declare-fun r58 () Real)
(declare-fun r59 () Real)
(declare-fun r60 () Real)
(declare-fun r61 () Real)
(declare-fun r62 () Real)
(declare-fun r63 () Real)
(declare-fun r64 () Real)
(declare-fun r65 () Real)
(declare-fun r66 () Real)
(declare-fun r67 () Real)
(declare-fun r68 () Real)
(declare-fun r69 () Real)
(declare-fun r70 () Real)
(declare-fun r71 () Real)
(declare-fun r72 () Real)
(declare-fun r73 () Real)
(declare-fun r74 () Real)
(declare-fun r75 () Real)
(declare-fun r76 () Real)
(declare-fun r77 () Real)
(declare-fun r78 () Real)
(declare-fun r79 () Real)
(declare-fun r80 () Real)
(declare-fun r81 () Real)
(declare-fun r82 () Real)
(declare-fun r83 () Real)
(declare-fun r84 () Real)
(declare-fun r85 () Real)
(declare-fun r86 () Real)
(declare-fun r87 () Real)
(declare-fun r88 () Real)
(declare-fun r89 () Real)
(declare-fun r90 () Real)
(declare-fun r91 () Real)
(declare-fun r92 () Real)
(declare-fun r93 () Real)
(declare-fun r94 () Real)
(declare-fun r95 () Real)
(declare-fun r96 () Real)
(declare-fun r97 () Real)
(declare-fun r98 () Real)
(declare-fun r99 () Real)
(declare-fun r100 () Real)
(declare-fun r101 () Real)
(declare-fun r102 () Real)
(declare-fun r103 () Real)
(declare-fun r104 () Real)
(declare-fun r105 () Real)
(declare-fun r106 () Real)
(declare-fun r107 () Real)
(declare-fun r108 () Real)
(declare-fun r109 () Real)
(declare-fun r110 () Real)
(declare-fun r111 () Real)
(declare-fun r112 () Real)
(declare-fun r113 () Real)
(declare-fun r114 () Real)
(declare-fun r115 () Real)
(declare-fun r116 () Real)
(declare-fun r117 () Real)
(declare-fun r118 () Real)
(declare-fun r119 () Real)
(declare-fun r120 () Real)
(declare-fun r121 () Real)
(declare-fun r122 () Real)
(declare-fun r123 () Real)
(declare-fun r124 () Real)
(declare-fun r125 () Real)
(declare-fun r126 () Real)
(declare-fun r127 () Real)
(declare-fun r128 () Real)
(declare-fun r129 () Real)
(declare-fun r130 () Real)
(declare-fun r131 () Real)
(declare-fun r132 () Real)
(declare-fun r133 () Real)
(declare-fun r134 () Real)
(declare-fun r135 () Real)
(declare-fun r136 () Real)
(declare-fun r137 () Real)
(declare-fun r138 () Real)
(declare-fun r139 () Real)
(declare-fun r140 () Real)
(declare-fun r141 () Real)
(declare-fun r142 () Real)
(declare-fun r143 () Real)
(declare-fun r144 () Real)
(declare-fun r145 () Real)
(declare-fun r146 () Real)
(declare-fun r147 () Real)
(declare-fun r148 () Real)
(declare-fun r149 () Real)
(declare-fun r150 () Real)
(declare-fun r151 () Real)
(declare-fun r152 () Real)
(declare-fun r153 () Real)
(declare-fun r154 () Real)
(declare-fun r155 () Real)
(declare-fun r156 () Real)
(declare-fun r157 () Real)
(declare-fun r158 () Real)
(declare-fun r159 () Real)
(declare-fun r160 () Real)
(declare-fun r161 () Real)
(declare-fun r162 () Real)
(declare-fun r163 () Real)
(declare-fun r164 () Real)
(declare-fun r165 () Real)
(declare-fun r166 () Real)
(declare-fun r167 () Real)
(declare-fun r168 () Real)
(declare-fun r169 () Real)
(declare-fun r170 () Real)
(declare-fun r171 () Real)
(declare-fun r172 () Real)
(declare-fun r173 () Real)
(declare-fun r174 () Real)
(declare-fun r175 () Real)
(declare-fun r176 () Real)
(declare-fun r177 () Real)
(declare-fun r178 () Real)
(declare-fun r179 () Real)
(declare-fun r180 () Real)
(declare-fun r181 () Real)
(declare-fun r182 () Real)
(declare-fun r183 () Real)
(declare-fun r184 () Real)
(declare-fun r185 () Real)
(declare-fun r186 () Real)
(declare-fun r187 () Real)
(declare-fun r188 () Real)
(declare-fun r189 () Real)
(declare-fun r190 () Real)
(declare-fun r191 () Real)
(declare-fun r192 () Real)
(declare-fun r193 () Real)
(declare-fun r194 () Real)
(declare-fun r195 () Real)
(declare-fun r196 () Real)
(declare-fun r197 () Real)
(declare-fun r198 () Real)
(declare-fun r199 () Real)
(declare-fun r200 () Real)
(declare-fun r201 () Real)
(declare-fun r202 () Real)
(declare-fun r203 () Real)
(declare-fun r204 () Real)
(declare-fun r205 () Real)
(declare-fun r206 () Real)
(declare-fun r207 () Real)
(declare-fun r208 () Real)
(declare-fun r209 () Real)
(declare-fun r210 () Real)
(declare-fun r211 () Real)
(declare-fun r212 () Real)
(declare-fun r213 () Real)
(declare-fun r214 () Real)
(declare-fun r215 () Real)
(declare-fun r216 () Real)
(declare-fun r217 () Real)
(declare-fun r218 () Real)
(declare-fun r219 () Real)
(declare-fun r220 () Real)
(declare-fun r221 () Real)
(declare-fun r222 () Real)
(declare-fun r223 () Real)
(declare-fun r224 () Real)
(declare-fun r225 () Real)
(declare-fun r226 () Real)
(declare-fun r227 () Real)
(assert (or (= r13 0) b14))
(assert (or (not b14) (= r13 1)))
(assert (or (not b14) b16))
(assert (or (not b14) (not b17)))
(assert (or (not b14) b18))
(assert (or (= r14 0) b20))
(assert (or (not b20) (= r14 1)))
(assert (or (not b20) b22))
(assert (or (not b20) (not b23)))
(assert (or b17 (not b20)))
(assert (or (not b20) b24))
(assert (or (= r15 0) b26))
(assert (or (not b26) (= r15 1)))
(assert (or (not b26) b28))
(assert (or (not b26) (not b29)))
(assert (or b23 (not b26)))
(assert (or (not b26) b30))
(assert (or (= r16 0) b32))
(assert (or (not b32) (= r16 1)))
(assert (or (not b32) b34))
(assert (or (not b32) (not b35)))
(assert (or b29 (not b32)))
(assert (or (not b32) b36))
(assert (or (= r18 0) b40))
(assert (or (not b40) (= r18 1)))
(assert (or b28 (not b40)))
(assert (or (not b40) (not b42)))
(assert (or (not b40) b43))
(assert (or (not b40) b44))
(assert (or (= r19 0) b46))
(assert (or (not b46) (= r19 1)))
(assert (or b34 (not b46)))
(assert (or (not b46) (not b48)))
(assert (or b42 (not b46)))
(assert (or (not b46) b49))
(assert (or (= r20 0) b51))
(assert (or (not b51) (= r20 1)))
(assert (or b38 (not b51)))
(assert (or (not b51) (not b53)))
(assert (or b48 (not b51)))
(assert (or (not b51) b54))
(assert (or (= r21 0) b56))
(assert (or (not b56) (= r21 1)))
(assert (or b28 (not b56)))
(assert (or (not b56) (not b58)))
(assert (or (not b56) b59))
(assert (or (not b56) b60))
(assert (or (= r22 0) b62))
(assert (or (not b62) (= r22 1)))
(assert (or b34 (not b62)))
(assert (or (not b62) (not b64)))
(assert (or b58 (not b62)))
(assert (or (not b62) b65))
(assert (or (= r23 0) b67))
(assert (or (not b67) (= r23 1)))
(assert (or b38 (not b67)))
(assert (or (not b67) (not b69)))
(assert (or b64 (not b67)))
(assert (or (not b67) b70))
(assert (or (= r24 0) b72))
(assert (or (not b72) (= r24 1)))
(assert (or (not b72) b74))
(assert (or (not b72) (not b75)))
(assert (or (not b72) b76))
(assert (or b30 (not b72)))
(assert (or (= r25 0) b78))
(assert (or (not b78) (= r25 1)))
(assert (or (not b78) b80))
(assert (or (not b78) (not b81)))
(assert (or b75 (not b78)))
(assert (or b36 (not b78)))
(assert (or (= r26 0) b83))
(assert (or (not b83) (= r26 1)))
(assert (or (not b83) b85))
(assert (or (not b83) (not b86)))
(assert (or b81 (not b83)))
(assert (or (not b83) b87))
(assert (or (= r27 0) b89))
(assert (or (not b89) (= r27 1)))
(assert (or (not b89) b91))
(assert (or (not b89) (not b92)))
(assert (or (not b89) b93))
(assert (or (= r28 0) b95))
(assert (or (not b95) (= r28 1)))
(assert (or (not b95) b97))
(assert (or (not b95) (not b98)))
(assert (or b92 (not b95)))
(assert (or (not b95) b99))
(assert (or (= r29 0) b101))
(assert (or (not b101) (= r29 1)))
(assert (or b74 (not b101)))
(assert (or (not b101) (not b103)))
(assert (or b98 (not b101)))
(assert (or b44 (not b101)))
(assert (or (= r30 0) b105))
(assert (or (not b105) (= r30 1)))
(assert (or b80 (not b105)))
(assert (or (not b105) (not b107)))
(assert (or b103 (not b105)))
(assert (or b49 (not b105)))
(assert (or (= r31 0) b109))
(assert (or (not b109) (= r31 1)))
(assert (or b85 (not b109)))
(assert (or (not b109) (not b111)))
(assert (or b107 (not b109)))
(assert (or b54 (not b109)))
(assert (or (= r32 0) b113))
(assert (or (not b113) (= r32 1)))
(assert (or b74 (not b113)))
(assert (or (not b113) (not b115)))
(assert (or (not b113) b116))
(assert (or b60 (not b113)))
(assert (or (= r33 0) b118))
(assert (or (not b118) (= r33 1)))
(assert (or b80 (not b118)))
(assert (or (not b118) (not b120)))
(assert (or b115 (not b118)))
(assert (or b65 (not b118)))
(assert (or (= r34 0) b122))
(assert (or (not b122) (= r34 1)))
(assert (or b85 (not b122)))
(assert (or (not b122) (not b124)))
(assert (or b120 (not b122)))
(assert (or b70 (not b122)))
(assert (or (= r35 0) b126))
(assert (or (not b126) (= r35 1)))
(assert (or (not b126) b128))
(assert (or (not b126) (not b129)))
(assert (or b18 (not b126)))
(assert (or (= r36 0) b131))
(assert (or (not b131) (= r36 1)))
(assert (or (not b131) b133))
(assert (or (not b131) (not b134)))
(assert (or b129 (not b131)))
(assert (or b24 (not b131)))
(assert (or (= r37 0) b136))
(assert (or (not b136) (= r37 1)))
(assert (or (not b136) b138))
(assert (or (not b136) (not b139)))
(assert (or b134 (not b136)))
(assert (or b30 (not b136)))
(assert (or (= r38 0) b141))
(assert (or (not b141) (= r38 1)))
(assert (or (not b141) b143))
(assert (or (not b141) (not b144)))
(assert (or b139 (not b141)))
(assert (or b36 (not b141)))
(assert (or (= r39 0) b146))
(assert (or (not b146) (= r39 1)))
(assert (or (not b146) b148))
(assert (or (not b146) (not b149)))
(assert (or b144 (not b146)))
(assert (or b87 (not b146)))
(assert (or (= r40 0) b151))
(assert (or (not b151) (= r40 1)))
(assert (or b138 (not b151)))
(assert (or (not b151) (not b153)))
(assert (or (not b151) b154))
(assert (or b44 (not b151)))
(assert (or (= r41 0) b156))
(assert (or (not b156) (= r41 1)))
(assert (or b143 (not b156)))
(assert (or (not b156) (not b158)))
(assert (or b153 (not b156)))
(assert (or b49 (not b156)))
(assert (or (= r43 0) b161))
(assert (or (not b161) (= r43 1)))
(assert (or b138 (not b161)))
(assert (or (not b161) (not b163)))
(assert (or (not b161) b164))
(assert (or b60 (not b161)))
(assert (or (= r44 0) b166))
(assert (or (not b166) (= r44 1)))
(assert (or b143 (not b166)))
(assert (or (not b166) (not b168)))
(assert (or b163 (not b166)))
(assert (or b65 (not b166)))
(assert (or (= r45 0) b170))
(assert (or (not b170) (= r45 1)))
(assert (or b148 (not b170)))
(assert (or (not b170) (not b172)))
(assert (or b168 (not b170)))
(assert (or b70 (not b170)))
(assert (or (= r46 0) b174))
(assert (or (not b174) (= r46 (- 1))))
(assert (or b23 (not b174)))
(assert (or (not b22) (not b174)))
(assert (or b16 (not b174)))
(assert (or b24 (not b174)))
(assert (or (= r47 0) b177))
(assert (or (not b177) (= r47 (- 1))))
(assert (or b29 (not b177)))
(assert (or (not b28) (not b177)))
(assert (or b22 (not b177)))
(assert (or b30 (not b177)))
(assert (or (= r48 0) b180))
(assert (or (not b180) (= r48 (- 1))))
(assert (or b35 (not b180)))
(assert (or (not b34) (not b180)))
(assert (or b28 (not b180)))
(assert (or b36 (not b180)))
(assert (or (= r49 0) b183))
(assert (or (not b183) (= r49 (- 1))))
(assert (or (not b38) (not b183)))
(assert (or b34 (not b183)))
(assert (or b87 (not b183)))
(assert (or (= r50 0) b186))
(assert (or (not b186) (= r50 (- 1))))
(assert (or b43 (not b186)))
(assert (or (not b22) (not b186)))
(assert (or b16 (not b186)))
(assert (or b99 (not b186)))
(assert (or (= r51 0) b189))
(assert (or (not b189) (= r51 (- 1))))
(assert (or b42 (not b189)))
(assert (or (not b28) (not b189)))
(assert (or b22 (not b189)))
(assert (or b44 (not b189)))
(assert (or (= r52 0) b192))
(assert (or (not b192) (= r52 (- 1))))
(assert (or b48 (not b192)))
(assert (or (not b34) (not b192)))
(assert (or b28 (not b192)))
(assert (or b49 (not b192)))
(assert (or (= r53 0) b195))
(assert (or (not b195) (= r53 (- 1))))
(assert (or b53 (not b195)))
(assert (or (not b38) (not b195)))
(assert (or b34 (not b195)))
(assert (or b54 (not b195)))
(assert (or (= r54 0) b198))
(assert (or (not b198) (= r54 (- 1))))
(assert (or b59 (not b198)))
(assert (or (not b22) (not b198)))
(assert (or b16 (not b198)))
(assert (or (not b198) b200))
(assert (or (= r55 0) b202))
(assert (or (not b202) (= r55 (- 1))))
(assert (or b58 (not b202)))
(assert (or (not b28) (not b202)))
(assert (or b22 (not b202)))
(assert (or b60 (not b202)))
(assert (or (= r56 0) b205))
(assert (or (not b205) (= r56 (- 1))))
(assert (or b64 (not b205)))
(assert (or (not b34) (not b205)))
(assert (or b28 (not b205)))
(assert (or b65 (not b205)))
(assert (or (= r57 0) b208))
(assert (or (not b208) (= r57 (- 1))))
(assert (or b69 (not b208)))
(assert (or (not b38) (not b208)))
(assert (or b34 (not b208)))
(assert (or b70 (not b208)))
(assert (or (= r58 0) b211))
(assert (or (not b211) (= r58 (- 1))))
(assert (or b76 (not b211)))
(assert (or (not b97) (not b211)))
(assert (or b91 (not b211)))
(assert (or b24 (not b211)))
(assert (or (= r59 0) b214))
(assert (or (not b214) (= r59 (- 1))))
(assert (or b75 (not b214)))
(assert (or (not b74) (not b214)))
(assert (or b97 (not b214)))
(assert (or b30 (not b214)))
(assert (or (= r60 0) b217))
(assert (or (not b217) (= r60 (- 1))))
(assert (or b81 (not b217)))
(assert (or (not b80) (not b217)))
(assert (or b74 (not b217)))
(assert (or b36 (not b217)))
(assert (or (= r61 0) b220))
(assert (or (not b220) (= r61 (- 1))))
(assert (or b86 (not b220)))
(assert (or (not b85) (not b220)))
(assert (or b80 (not b220)))
(assert (or b87 (not b220)))
(assert (or (= r62 0) b223))
(assert (or (not b223) (= r62 (- 1))))
(assert (or b98 (not b223)))
(assert (or (not b97) (not b223)))
(assert (or b91 (not b223)))
(assert (or b99 (not b223)))
(assert (or (= r63 0) b226))
(assert (or (not b226) (= r63 (- 1))))
(assert (or b103 (not b226)))
(assert (or (not b74) (not b226)))
(assert (or b97 (not b226)))
(assert (or b44 (not b226)))
(assert (or (= r64 0) b229))
(assert (or (not b229) (= r64 (- 1))))
(assert (or b107 (not b229)))
(assert (or (not b80) (not b229)))
(assert (or b74 (not b229)))
(assert (or b49 (not b229)))
(assert (or (= r65 0) b232))
(assert (or (not b232) (= r65 (- 1))))
(assert (or b111 (not b232)))
(assert (or (not b85) (not b232)))
(assert (or b80 (not b232)))
(assert (or b54 (not b232)))
(assert (or (= r66 0) b235))
(assert (or (not b235) (= r66 (- 1))))
(assert (or b116 (not b235)))
(assert (or (not b97) (not b235)))
(assert (or b91 (not b235)))
(assert (or b200 (not b235)))
(assert (or (= r67 0) b238))
(assert (or (not b238) (= r67 (- 1))))
(assert (or b115 (not b238)))
(assert (or (not b74) (not b238)))
(assert (or b97 (not b238)))
(assert (or b60 (not b238)))
(assert (or (= r68 0) b241))
(assert (or (not b241) (= r68 (- 1))))
(assert (or b120 (not b241)))
(assert (or (not b80) (not b241)))
(assert (or b74 (not b241)))
(assert (or b65 (not b241)))
(assert (or (= r69 0) b244))
(assert (or (not b244) (= r69 (- 1))))
(assert (or b124 (not b244)))
(assert (or (not b85) (not b244)))
(assert (or b80 (not b244)))
(assert (or b70 (not b244)))
(assert (or (= r70 0) b247))
(assert (or (not b247) (= r70 (- 1))))
(assert (or b134 (not b247)))
(assert (or (not b133) (not b247)))
(assert (or b128 (not b247)))
(assert (or b24 (not b247)))
(assert (or (= r71 0) b250))
(assert (or (not b250) (= r71 (- 1))))
(assert (or b139 (not b250)))
(assert (or (not b138) (not b250)))
(assert (or b133 (not b250)))
(assert (or b30 (not b250)))
(assert (or (= r72 0) b253))
(assert (or (not b253) (= r72 (- 1))))
(assert (or b144 (not b253)))
(assert (or (not b143) (not b253)))
(assert (or b138 (not b253)))
(assert (or b36 (not b253)))
(assert (or (= r73 0) b256))
(assert (or (not b256) (= r73 (- 1))))
(assert (or b149 (not b256)))
(assert (or (not b148) (not b256)))
(assert (or b143 (not b256)))
(assert (or b87 (not b256)))
(assert (or (= r74 0) b259))
(assert (or (not b259) (= r74 (- 1))))
(assert (or b154 (not b259)))
(assert (or (not b133) (not b259)))
(assert (or b128 (not b259)))
(assert (or b99 (not b259)))
(assert (or (= r75 0) b262))
(assert (or (not b262) (= r75 (- 1))))
(assert (or b153 (not b262)))
(assert (or (not b138) (not b262)))
(assert (or b133 (not b262)))
(assert (or b44 (not b262)))
(assert (or (= r76 0) b265))
(assert (or (not b265) (= r76 (- 1))))
(assert (or b158 (not b265)))
(assert (or (not b143) (not b265)))
(assert (or b138 (not b265)))
(assert (or b49 (not b265)))
(assert (or (= r77 0) b268))
(assert (or (not b268) (= r77 (- 1))))
(assert (or (not b148) (not b268)))
(assert (or b143 (not b268)))
(assert (or b54 (not b268)))
(assert (or (= r78 0) b271))
(assert (or (not b271) (= r78 (- 1))))
(assert (or b164 (not b271)))
(assert (or (not b133) (not b271)))
(assert (or b128 (not b271)))
(assert (or b200 (not b271)))
(assert (or (= r79 0) b274))
(assert (or (not b274) (= r79 (- 1))))
(assert (or b163 (not b274)))
(assert (or (not b138) (not b274)))
(assert (or b133 (not b274)))
(assert (or b60 (not b274)))
(assert (or (= r80 0) b277))
(assert (or (not b277) (= r80 (- 1))))
(assert (or b168 (not b277)))
(assert (or (not b143) (not b277)))
(assert (or b138 (not b277)))
(assert (or b65 (not b277)))
(assert (or (= r81 0) b280))
(assert (or (not b280) (= r81 (- 1))))
(assert (or b172 (not b280)))
(assert (or (not b148) (not b280)))
(assert (or b143 (not b280)))
(assert (or b70 (not b280)))
(assert (or (= r82 0) b283))
(assert (or b283 (= r83 0)))
(assert (or (not b283) (= r83 (* (- 631) 3))))
(assert (or (not b283) (= r82 (* 631 3))))
(assert (or b99 (not b283)))
(assert (or (not b24) (not b283)))
(assert (or b18 (not b283)))
(assert (or (not b283) (>= r84 (* 631 3))))
(assert (or (= r85 0) b289))
(assert (or b289 (= r86 0)))
(assert (or (not b289) (= r86 (* (- 631) 3))))
(assert (or (not b289) (= r85 (* 631 3))))
(assert (or b44 (not b289)))
(assert (or (not b30) (not b289)))
(assert (or b24 (not b289)))
(assert (or (not b289) (>= r87 (* 631 3))))
(assert (or (= r88 0) b295))
(assert (or b295 (= r89 0)))
(assert (or (not b295) (= r89 (* (- 631) 3))))
(assert (or (not b295) (= r88 (* 631 3))))
(assert (or b49 (not b295)))
(assert (or (not b36) (not b295)))
(assert (or b30 (not b295)))
(assert (or (not b295) (>= r90 (* 631 3))))
(assert (or (= r91 0) b301))
(assert (or b301 (= r92 0)))
(assert (or (not b301) (= r92 (* (- 631) 3))))
(assert (or (not b301) (= r91 (* 631 3))))
(assert (or b54 (not b301)))
(assert (or (not b87) (not b301)))
(assert (or b36 (not b301)))
(assert (or (not b301) (>= r93 (* 631 3))))
(assert (or (= r96 0) b310))
(assert (or b310 (= r97 0)))
(assert (or (not b310) (= r97 (* (- 998) 3))))
(assert (or (not b310) (= r96 (* 998 3))))
(assert (or b200 (not b310)))
(assert (or (not b24) (not b310)))
(assert (or b18 (not b310)))
(assert (or (not b310) (>= r84 (* 998 3))))
(assert (or (= r98 0) b316))
(assert (or b316 (= r99 0)))
(assert (or (not b316) (= r99 (* (- 998) 3))))
(assert (or (not b316) (= r98 (* 998 3))))
(assert (or b60 (not b316)))
(assert (or (not b30) (not b316)))
(assert (or b24 (not b316)))
(assert (or (not b316) (>= r87 (* 998 3))))
(assert (or (= r100 0) b322))
(assert (or b322 (= r101 0)))
(assert (or (not b322) (= r101 (* (- 998) 3))))
(assert (or (not b322) (= r100 (* 998 3))))
(assert (or b65 (not b322)))
(assert (or (not b36) (not b322)))
(assert (or b30 (not b322)))
(assert (or (not b322) (>= r90 (* 998 3))))
(assert (or (= r102 0) b328))
(assert (or b328 (= r103 0)))
(assert (or (not b328) (= r103 (* (- 998) 3))))
(assert (or (not b328) (= r102 (* 998 3))))
(assert (or b70 (not b328)))
(assert (or (not b87) (not b328)))
(assert (or b36 (not b328)))
(assert (or (not b328) (>= r93 (* 998 3))))
(assert (or (= r106 0) b337))
(assert (or b337 (= r107 0)))
(assert (or (not b337) (= r107 (* (- 631) 3))))
(assert (or (not b337) (= r106 (* 631 3))))
(assert (or b24 (not b337)))
(assert (or (not b99) (not b337)))
(assert (or b93 (not b337)))
(assert (or (>= r84 (* 631 3)) (not b337)))
(assert (or (= r108 0) b342))
(assert (or b342 (= r109 0)))
(assert (or (not b342) (= r109 (* (- 631) 3))))
(assert (or (not b342) (= r108 (* 631 3))))
(assert (or b30 (not b342)))
(assert (or (not b44) (not b342)))
(assert (or b99 (not b342)))
(assert (or (>= r87 (* 631 3)) (not b342)))
(assert (or (= r110 0) b347))
(assert (or b347 (= r111 0)))
(assert (or (not b347) (= r111 (* (- 631) 3))))
(assert (or (not b347) (= r110 (* 631 3))))
(assert (or b36 (not b347)))
(assert (or (not b49) (not b347)))
(assert (or b44 (not b347)))
(assert (or (>= r90 (* 631 3)) (not b347)))
(assert (or (= r112 0) b352))
(assert (or b352 (= r113 0)))
(assert (or (not b352) (= r113 (* (- 631) 3))))
(assert (or (not b352) (= r112 (* 631 3))))
(assert (or b87 (not b352)))
(assert (or (not b54) (not b352)))
(assert (or b49 (not b352)))
(assert (or (>= r93 (* 631 3)) (not b352)))
(assert (or (= r114 0) b357))
(assert (or b357 (= r115 0)))
(assert (or (not b357) (= r115 (* (- 631) 3))))
(assert (or (not b357) (= r114 (* 631 3))))
(assert (or (not b308) (not b357)))
(assert (or b54 (not b357)))
(assert (or (not b357) (>= r116 (* 631 3))))
(assert (or (= r117 0) b363))
(assert (or b363 (= r118 0)))
(assert (or (not b363) (= r118 (* (- 627) 3))))
(assert (or (not b363) (= r117 (* 627 3))))
(assert (or b200 (not b363)))
(assert (or (not b99) (not b363)))
(assert (or b93 (not b363)))
(assert (or (not b363) (>= r84 (* 627 3))))
(assert (or (= r119 0) b369))
(assert (or b369 (= r120 0)))
(assert (or (not b369) (= r120 (* (- 627) 3))))
(assert (or (not b369) (= r119 (* 627 3))))
(assert (or b60 (not b369)))
(assert (or (not b44) (not b369)))
(assert (or b99 (not b369)))
(assert (or (not b369) (>= r87 (* 627 3))))
(assert (or (= r121 0) b375))
(assert (or b375 (= r122 0)))
(assert (or (not b375) (= r122 (* (- 627) 3))))
(assert (or (not b375) (= r121 (* 627 3))))
(assert (or b65 (not b375)))
(assert (or (not b49) (not b375)))
(assert (or b44 (not b375)))
(assert (or (not b375) (>= r90 (* 627 3))))
(assert (or (= r123 0) b381))
(assert (or b381 (= r124 0)))
(assert (or (not b381) (= r124 (* (- 627) 3))))
(assert (or (not b381) (= r123 (* 627 3))))
(assert (or b70 (not b381)))
(assert (or (not b54) (not b381)))
(assert (or b49 (not b381)))
(assert (or (not b381) (>= r93 (* 627 3))))
(assert (or (= r125 0) b387))
(assert (or b387 (= r126 0)))
(assert (or (not b387) (= r126 (* (- 627) 3))))
(assert (or (not b387) (= r125 (* 627 3))))
(assert (or b335 (not b387)))
(assert (or (not b308) (not b387)))
(assert (or b54 (not b387)))
(assert (or (not b387) (>= r116 (* 627 3))))
(assert (or (= r127 0) b393))
(assert (or b393 (= r128 0)))
(assert (or (not b393) (= r128 (* (- 998) 3))))
(assert (or (not b393) (= r127 (* 998 3))))
(assert (or b18 (not b393)))
(assert (or (not b393) (not b397)))
(assert (or (not b393) (>= r11 (* 998 3))))
(assert (or (= r129 0) b400))
(assert (or b400 (= r130 0)))
(assert (or (not b400) (= r130 (* (- 998) 3))))
(assert (or (not b400) (= r129 (* 998 3))))
(assert (or b24 (not b400)))
(assert (or (not b200) (not b400)))
(assert (or b397 (not b400)))
(assert (or (>= r84 (* 998 3)) (not b400)))
(assert (or (= r131 0) b405))
(assert (or b405 (= r132 0)))
(assert (or (not b405) (= r132 (* (- 998) 3))))
(assert (or (not b405) (= r131 (* 998 3))))
(assert (or b30 (not b405)))
(assert (or (not b60) (not b405)))
(assert (or b200 (not b405)))
(assert (or (>= r87 (* 998 3)) (not b405)))
(assert (or (= r133 0) b410))
(assert (or b410 (= r134 0)))
(assert (or (not b410) (= r134 (* (- 998) 3))))
(assert (or (not b410) (= r133 (* 998 3))))
(assert (or b36 (not b410)))
(assert (or (not b65) (not b410)))
(assert (or b60 (not b410)))
(assert (or (>= r90 (* 998 3)) (not b410)))
(assert (or (= r135 0) b415))
(assert (or b415 (= r136 0)))
(assert (or (not b415) (= r136 (* (- 998) 3))))
(assert (or (not b415) (= r135 (* 998 3))))
(assert (or b87 (not b415)))
(assert (or (not b70) (not b415)))
(assert (or b65 (not b415)))
(assert (or (>= r93 (* 998 3)) (not b415)))
(assert (or (= r137 0) b420))
(assert (or b420 (= r138 0)))
(assert (or (not b420) (= r138 (* (- 998) 3))))
(assert (or (not b420) (= r137 (* 998 3))))
(assert (or (not b335) (not b420)))
(assert (or b70 (not b420)))
(assert (or (not b420) (>= r116 (* 998 3))))
(assert (or (= r139 0) b426))
(assert (or b426 (= r140 0)))
(assert (or (not b426) (= r140 (* (- 627) 3))))
(assert (or (not b426) (= r139 (* 627 3))))
(assert (or b93 (not b426)))
(assert (or (not b397) (not b426)))
(assert (or (not b426) (>= r11 (* 627 3))))
(assert (or (= r141 0) b432))
(assert (or b432 (= r142 0)))
(assert (or (not b432) (= r142 (* (- 627) 3))))
(assert (or (not b432) (= r141 (* 627 3))))
(assert (or b99 (not b432)))
(assert (or (not b200) (not b432)))
(assert (or b397 (not b432)))
(assert (or (>= r84 (* 627 3)) (not b432)))
(assert (or (= r143 0) b437))
(assert (or b437 (= r144 0)))
(assert (or (not b437) (= r144 (* (- 627) 3))))
(assert (or (not b437) (= r143 (* 627 3))))
(assert (or b44 (not b437)))
(assert (or (not b60) (not b437)))
(assert (or b200 (not b437)))
(assert (or (>= r87 (* 627 3)) (not b437)))
(assert (or (= r145 0) b442))
(assert (or b442 (= r146 0)))
(assert (or (not b442) (= r146 (* (- 627) 3))))
(assert (or (not b442) (= r145 (* 627 3))))
(assert (or b49 (not b442)))
(assert (or (not b65) (not b442)))
(assert (or b60 (not b442)))
(assert (or (>= r90 (* 627 3)) (not b442)))
(assert (or (= r147 0) b447))
(assert (or b447 (= r148 0)))
(assert (or (not b447) (= r148 (* (- 627) 3))))
(assert (or (not b447) (= r147 (* 627 3))))
(assert (or b54 (not b447)))
(assert (or (not b70) (not b447)))
(assert (or b65 (not b447)))
(assert (or (>= r93 (* 627 3)) (not b447)))
(assert (or (= r149 0) b452))
(assert (or b452 (= r150 0)))
(assert (or (not b452) (= r150 (* (- 627) 3))))
(assert (or (not b452) (= r149 (* 627 3))))
(assert (or b308 (not b452)))
(assert (or (not b335) (not b452)))
(assert (or b70 (not b452)))
(assert (or (>= r116 (* 627 3)) (not b452)))
(assert (or (= r151 0) b457))
(assert (or b457 (= r152 0)))
(assert (or (not b457) (= r152 (* (- 631) 11))))
(assert (or (not b457) (= r151 (* 631 11))))
(assert (or b99 (not b457)))
(assert (or (not b24) (not b457)))
(assert (or b18 (not b457)))
(assert (or (not b457) (>= r84 (* 631 11))))
(assert (or (not b457) (<= r153 9)))
(assert (or (= r154 0) b464))
(assert (or b464 (= r155 0)))
(assert (or (not b464) (= r155 (* (- 631) 11))))
(assert (or (not b464) (= r154 (* 631 11))))
(assert (or b44 (not b464)))
(assert (or (not b30) (not b464)))
(assert (or b24 (not b464)))
(assert (or (not b464) (>= r87 (* 631 11))))
(assert (or (not b464) (<= r156 9)))
(assert (or (= r157 0) b471))
(assert (or b471 (= r158 0)))
(assert (or (not b471) (= r158 (* (- 631) 11))))
(assert (or (not b471) (= r157 (* 631 11))))
(assert (or b49 (not b471)))
(assert (or (not b36) (not b471)))
(assert (or b30 (not b471)))
(assert (or (not b471) (>= r90 (* 631 11))))
(assert (or (not b471) (<= r159 9)))
(assert (or (= r160 0) b478))
(assert (or b478 (= r161 0)))
(assert (or (not b478) (= r161 (* (- 631) 11))))
(assert (or (not b478) (= r160 (* 631 11))))
(assert (or b54 (not b478)))
(assert (or (not b87) (not b478)))
(assert (or b36 (not b478)))
(assert (or (not b478) (>= r93 (* 631 11))))
(assert (or (not b478) (<= r162 9)))
(assert (or (= r165 0) b487))
(assert (or b487 (= r166 0)))
(assert (or (not b487) (= r166 (* (- 998) 11))))
(assert (or (not b487) (= r165 (* 998 11))))
(assert (or b200 (not b487)))
(assert (or (not b24) (not b487)))
(assert (or b18 (not b487)))
(assert (or (not b487) (>= r84 (* 998 11))))
(assert (or (<= r153 9) (not b487)))
(assert (or (= r167 0) b493))
(assert (or b493 (= r168 0)))
(assert (or (not b493) (= r168 (* (- 998) 11))))
(assert (or (not b493) (= r167 (* 998 11))))
(assert (or b60 (not b493)))
(assert (or (not b30) (not b493)))
(assert (or b24 (not b493)))
(assert (or (not b493) (>= r87 (* 998 11))))
(assert (or (<= r156 9) (not b493)))
(assert (or (= r169 0) b499))
(assert (or b499 (= r170 0)))
(assert (or (not b499) (= r170 (* (- 998) 11))))
(assert (or (not b499) (= r169 (* 998 11))))
(assert (or b65 (not b499)))
(assert (or (not b36) (not b499)))
(assert (or b30 (not b499)))
(assert (or (not b499) (>= r90 (* 998 11))))
(assert (or (<= r159 9) (not b499)))
(assert (or (= r171 0) b505))
(assert (or b505 (= r172 0)))
(assert (or (not b505) (= r172 (* (- 998) 11))))
(assert (or (not b505) (= r171 (* 998 11))))
(assert (or b70 (not b505)))
(assert (or (not b87) (not b505)))
(assert (or b36 (not b505)))
(assert (or (not b505) (>= r93 (* 998 11))))
(assert (or (<= r162 9) (not b505)))
(assert (or (= r175 0) b513))
(assert (or b513 (= r176 0)))
(assert (or (not b513) (= r176 (* (- 631) 11))))
(assert (or (not b513) (= r175 (* 631 11))))
(assert (or b24 (not b513)))
(assert (or (not b99) (not b513)))
(assert (or b93 (not b513)))
(assert (or (>= r84 (* 631 11)) (not b513)))
(assert (or (<= r153 9) (not b513)))
(assert (or (= r177 0) b518))
(assert (or b518 (= r178 0)))
(assert (or (not b518) (= r178 (* (- 631) 11))))
(assert (or (not b518) (= r177 (* 631 11))))
(assert (or b30 (not b518)))
(assert (or (not b44) (not b518)))
(assert (or b99 (not b518)))
(assert (or (>= r87 (* 631 11)) (not b518)))
(assert (or (<= r156 9) (not b518)))
(assert (or (= r179 0) b523))
(assert (or b523 (= r180 0)))
(assert (or (not b523) (= r180 (* (- 631) 11))))
(assert (or (not b523) (= r179 (* 631 11))))
(assert (or b36 (not b523)))
(assert (or (not b49) (not b523)))
(assert (or b44 (not b523)))
(assert (or (>= r90 (* 631 11)) (not b523)))
(assert (or (<= r159 9) (not b523)))
(assert (or (= r181 0) b528))
(assert (or b528 (= r182 0)))
(assert (or (not b528) (= r182 (* (- 631) 11))))
(assert (or (not b528) (= r181 (* 631 11))))
(assert (or b87 (not b528)))
(assert (or (not b54) (not b528)))
(assert (or b49 (not b528)))
(assert (or (>= r93 (* 631 11)) (not b528)))
(assert (or (<= r162 9) (not b528)))
(assert (or (= r183 0) b533))
(assert (or b533 (= r184 0)))
(assert (or (not b533) (= r184 (* (- 631) 11))))
(assert (or (not b533) (= r183 (* 631 11))))
(assert (or (not b308) (not b533)))
(assert (or b54 (not b533)))
(assert (or (not b533) (>= r116 (* 631 11))))
(assert (or (not b533) (<= r185 9)))
(assert (or (= r186 0) b540))
(assert (or b540 (= r187 0)))
(assert (or (not b540) (= r187 (* (- 627) 11))))
(assert (or (not b540) (= r186 (* 627 11))))
(assert (or b200 (not b540)))
(assert (or (not b99) (not b540)))
(assert (or b93 (not b540)))
(assert (or (not b540) (>= r84 (* 627 11))))
(assert (or (<= r153 9) (not b540)))
(assert (or (= r188 0) b546))
(assert (or b546 (= r189 0)))
(assert (or (not b546) (= r189 (* (- 627) 11))))
(assert (or (not b546) (= r188 (* 627 11))))
(assert (or b60 (not b546)))
(assert (or (not b44) (not b546)))
(assert (or b99 (not b546)))
(assert (or (not b546) (>= r87 (* 627 11))))
(assert (or (<= r156 9) (not b546)))
(assert (or (= r190 0) b552))
(assert (or b552 (= r191 0)))
(assert (or (not b552) (= r191 (* (- 627) 11))))
(assert (or (not b552) (= r190 (* 627 11))))
(assert (or b65 (not b552)))
(assert (or (not b49) (not b552)))
(assert (or b44 (not b552)))
(assert (or (not b552) (>= r90 (* 627 11))))
(assert (or (<= r159 9) (not b552)))
(assert (or (= r192 0) b558))
(assert (or b558 (= r193 0)))
(assert (or (not b558) (= r193 (* (- 627) 11))))
(assert (or (not b558) (= r192 (* 627 11))))
(assert (or b70 (not b558)))
(assert (or (not b54) (not b558)))
(assert (or b49 (not b558)))
(assert (or (not b558) (>= r93 (* 627 11))))
(assert (or (<= r162 9) (not b558)))
(assert (or (= r194 0) b564))
(assert (or b564 (= r195 0)))
(assert (or (not b564) (= r195 (* (- 627) 11))))
(assert (or (not b564) (= r194 (* 627 11))))
(assert (or b335 (not b564)))
(assert (or (not b308) (not b564)))
(assert (or b54 (not b564)))
(assert (or (not b564) (>= r116 (* 627 11))))
(assert (or (<= r185 9) (not b564)))
(assert (or (= r196 0) b570))
(assert (or b570 (= r197 0)))
(assert (or (not b570) (= r197 (* (- 998) 11))))
(assert (or (not b570) (= r196 (* 998 11))))
(assert (or b18 (not b570)))
(assert (or (not b397) (not b570)))
(assert (or (not b570) (>= r11 (* 998 11))))
(assert (or (not b570) (<= r10 9)))
(assert (or (= r198 0) b577))
(assert (or b577 (= r199 0)))
(assert (or (not b577) (= r199 (* (- 998) 11))))
(assert (or (not b577) (= r198 (* 998 11))))
(assert (or b24 (not b577)))
(assert (or (not b200) (not b577)))
(assert (or b397 (not b577)))
(assert (or (>= r84 (* 998 11)) (not b577)))
(assert (or (<= r153 9) (not b577)))
(assert (or (= r200 0) b582))
(assert (or b582 (= r201 0)))
(assert (or (not b582) (= r201 (* (- 998) 11))))
(assert (or (not b582) (= r200 (* 998 11))))
(assert (or b30 (not b582)))
(assert (or (not b60) (not b582)))
(assert (or b200 (not b582)))
(assert (or (>= r87 (* 998 11)) (not b582)))
(assert (or (<= r156 9) (not b582)))
(assert (or (= r202 0) b587))
(assert (or b587 (= r203 0)))
(assert (or (not b587) (= r203 (* (- 998) 11))))
(assert (or (not b587) (= r202 (* 998 11))))
(assert (or b36 (not b587)))
(assert (or (not b65) (not b587)))
(assert (or b60 (not b587)))
(assert (or (>= r90 (* 998 11)) (not b587)))
(assert (or (<= r159 9) (not b587)))
(assert (or (= r204 0) b592))
(assert (or b592 (= r205 0)))
(assert (or (not b592) (= r205 (* (- 998) 11))))
(assert (or (not b592) (= r204 (* 998 11))))
(assert (or b87 (not b592)))
(assert (or (not b70) (not b592)))
(assert (or b65 (not b592)))
(assert (or (>= r93 (* 998 11)) (not b592)))
(assert (or (<= r162 9) (not b592)))
(assert (or (= r206 0) b597))
(assert (or b597 (= r207 0)))
(assert (or (not b597) (= r207 (* (- 998) 11))))
(assert (or (not b597) (= r206 (* 998 11))))
(assert (or (not b335) (not b597)))
(assert (or b70 (not b597)))
(assert (or (not b597) (>= r116 (* 998 11))))
(assert (or (<= r185 9) (not b597)))
(assert (or (= r208 0) b603))
(assert (or b603 (= r209 0)))
(assert (or (not b603) (= r209 (* (- 627) 11))))
(assert (or (not b603) (= r208 (* 627 11))))
(assert (or b93 (not b603)))
(assert (or (not b397) (not b603)))
(assert (or (not b603) (>= r11 (* 627 11))))
(assert (or (<= r10 9) (not b603)))
(assert (or (= r210 0) b609))
(assert (or b609 (= r211 0)))
(assert (or (not b609) (= r211 (* (- 627) 11))))
(assert (or (not b609) (= r210 (* 627 11))))
(assert (or b99 (not b609)))
(assert (or (not b200) (not b609)))
(assert (or b397 (not b609)))
(assert (or (>= r84 (* 627 11)) (not b609)))
(assert (or (<= r153 9) (not b609)))
(assert (or (= r212 0) b614))
(assert (or b614 (= r213 0)))
(assert (or (not b614) (= r213 (* (- 627) 11))))
(assert (or (not b614) (= r212 (* 627 11))))
(assert (or b44 (not b614)))
(assert (or (not b60) (not b614)))
(assert (or b200 (not b614)))
(assert (or (>= r87 (* 627 11)) (not b614)))
(assert (or (<= r156 9) (not b614)))
(assert (or (= r214 0) b619))
(assert (or b619 (= r215 0)))
(assert (or (not b619) (= r215 (* (- 627) 11))))
(assert (or (not b619) (= r214 (* 627 11))))
(assert (or b49 (not b619)))
(assert (or (not b65) (not b619)))
(assert (or b60 (not b619)))
(assert (or (>= r90 (* 627 11)) (not b619)))
(assert (or (<= r159 9) (not b619)))
(assert (or (= r216 0) b624))
(assert (or b624 (= r217 0)))
(assert (or (not b624) (= r217 (* (- 627) 11))))
(assert (or (not b624) (= r216 (* 627 11))))
(assert (or b54 (not b624)))
(assert (or (not b70) (not b624)))
(assert (or b65 (not b624)))
(assert (or (>= r93 (* 627 11)) (not b624)))
(assert (or (<= r162 9) (not b624)))
(assert (or (= r218 0) b629))
(assert (or b629 (= r219 0)))
(assert (or (not b629) (= r219 (* (- 627) 11))))
(assert (or (not b629) (= r218 (* 627 11))))
(assert (or b308 (not b629)))
(assert (or (not b335) (not b629)))
(assert (or b70 (not b629)))
(assert (or (>= r116 (* 627 11)) (not b629)))
(assert (or (<= r185 9) (not b629)))
(assert (or (not b633) (= r87 6830)))
(assert (or (not b633) (< (+ r84 r220) 6830)))
(assert (or b18 (not b633)))
(assert (or (not b636) (= r90 6830)))
(assert (or (not b636) (< (+ r87 r220) 6830)))
(assert (or b24 (not b636)))
(assert (or (not b639) (= r93 6830)))
(assert (or (not b639) (< (+ r90 r220) 6830)))
(assert (or b30 (not b639)))
(assert (or (not b642) (= r116 6830)))
(assert (or (not b642) (< (+ r93 r220) 6830)))
(assert (or b36 (not b642)))
(assert (or (not b645) (= r221 6830)))
(assert (or (not b645) (< (+ r116 r220) 6830)))
(assert (or b87 (not b645)))
(assert (or (= r87 6830) (not b648)))
(assert (or (< (+ r84 r220) 6830) (not b648)))
(assert (or b93 (not b648)))
(assert (or (= r90 6830) (not b649)))
(assert (or (< (+ r87 r220) 6830) (not b649)))
(assert (or b99 (not b649)))
(assert (or (= r93 6830) (not b650)))
(assert (or (< (+ r90 r220) 6830) (not b650)))
(assert (or b44 (not b650)))
(assert (or (= r116 6830) (not b651)))
(assert (or (< (+ r93 r220) 6830) (not b651)))
(assert (or b49 (not b651)))
(assert (or (= r221 6830) (not b652)))
(assert (or (< (+ r116 r220) 6830) (not b652)))
(assert (or b54 (not b652)))
(assert (or (not b653) (= r84 6830)))
(assert (or (not b653) (< (+ r11 r220) 6830)))
(assert (or (= r87 6830) (not b656)))
(assert (or (< (+ r84 r220) 6830) (not b656)))
(assert (or b397 (not b656)))
(assert (or (= r90 6830) (not b657)))
(assert (or (< (+ r87 r220) 6830) (not b657)))
(assert (or b200 (not b657)))
(assert (or (= r93 6830) (not b658)))
(assert (or (< (+ r90 r220) 6830) (not b658)))
(assert (or b60 (not b658)))
(assert (or (= r116 6830) (not b659)))
(assert (or (< (+ r93 r220) 6830) (not b659)))
(assert (or b65 (not b659)))
(assert (or (= r221 6830) (not b660)))
(assert (or (< (+ r116 r220) 6830) (not b660)))
(assert (or b70 (not b660)))
(assert (or (or (or (or b393 b397) b426) b570) b603))
(assert (or (or (or (or (or (not b200) b310) b363) b397) b487) b540))
(assert (or (or (or (or (or b200 (not b397)) b400) b432) b577) b609))
(assert (or (or (or (or (or (not b60) b200) b316) b369) b493) b546))
(assert (or (or (or (or (or b60 (not b200)) b405) b437) b582) b614))
(assert (or (or (or (or (or b60 (not b65)) b322) b375) b499) b552))
(assert (or (or (or (or (or (not b60) b65) b410) b442) b587) b619))
(assert (or (or (or (or (or b65 (not b70)) b328) b381) b505) b558))
(assert (or (or (or (or (or (not b65) b70) b415) b447) b592) b624))
(assert (or (or (or b70 (not b335)) b387) b564))
(assert (or (or (or (or (or (not b70) b335) b420) b452) b597) b629))
(assert (or (or (not b93) b426) b603))
(assert (or (or (or (or (or b93 (not b99)) b283) b432) b457) b609))
(assert (or (or (or (or (or (not b93) b99) b337) b363) b513) b540))
(assert (or (or (or (or (or (not b44) b99) b289) b437) b464) b614))
(assert (or (or (or (or (or b44 (not b99)) b342) b369) b518) b546))
(assert (or (or (or (or (or b44 (not b49)) b295) b442) b471) b619))
(assert (or (or (or (or (or (not b44) b49) b347) b375) b523) b552))
(assert (or (or (or (or (or b49 (not b54)) b301) b447) b478) b624))
(assert (or (or (or (or (or (not b49) b54) b352) b381) b528) b558))
(assert (or (or (or b54 (not b308)) b452) b629))
(assert (or (or (or (or (or (not b54) b308) b357) b387) b533) b564))
(assert (or (or (not b18) b393) b570))
(assert (or (or (or (or (or b18 (not b24)) b337) b400) b513) b577))
(assert (or (or (or (or (or (not b18) b24) b283) b310) b457) b487))
(assert (or (or (or (or (or b24 (not b30)) b342) b405) b518) b582))
(assert (or (or (or (or (or (not b24) b30) b289) b316) b464) b493))
(assert (or (or (or (or (or b30 (not b36)) b347) b410) b523) b587))
(assert (or (or (or (or (or (not b30) b36) b295) b322) b471) b499))
(assert (or (or (or (or (or b36 (not b87)) b352) b415) b528) b592))
(assert (or (or (or (or (or (not b36) b87) b301) b328) b478) b505))
(assert (or (or (or (or b87 b357) b420) b533) b597))
(assert (or (not b164) b271))
(assert (or (or (not b163) b164) b274))
(assert (or (or b161 b163) (not b164)))
(assert (or (or b163 (not b168)) b277))
(assert (or (or (not b163) b166) b168))
(assert (or (or b168 (not b172)) b280))
(assert (or (or (not b168) b170) b172))
(assert (or (not b154) b259))
(assert (or (or (not b153) b154) b262))
(assert (or (or b151 b153) (not b154)))
(assert (or (or b153 (not b158)) b265))
(assert (or (or (not b153) b156) b158))
(assert (or b158 b268))
(assert (or b126 b129))
(assert (or (or b129 (not b134)) b247))
(assert (or (or (not b129) b131) b134))
(assert (or (or b134 (not b139)) b250))
(assert (or (or (not b134) b136) b139))
(assert (or (or b139 (not b144)) b253))
(assert (or (or (not b139) b141) b144))
(assert (or (or b144 (not b149)) b256))
(assert (or (or (not b144) b146) b149))
(assert (or (not b116) b235))
(assert (or (or (not b115) b116) b238))
(assert (or (or b113 b115) (not b116)))
(assert (or (or b115 (not b120)) b241))
(assert (or (or (not b115) b118) b120))
(assert (or (or b120 (not b124)) b244))
(assert (or (or (not b120) b122) b124))
(assert (or b89 b92))
(assert (or (or b92 (not b98)) b223))
(assert (or (or (not b92) b95) b98))
(assert (or (or b98 (not b103)) b226))
(assert (or (or (not b98) b101) b103))
(assert (or (or b103 (not b107)) b229))
(assert (or (or (not b103) b105) b107))
(assert (or (or b107 (not b111)) b232))
(assert (or (or (not b107) b109) b111))
(assert (or (not b76) b211))
(assert (or (or (not b75) b76) b214))
(assert (or (or b72 b75) (not b76)))
(assert (or (or b75 (not b81)) b217))
(assert (or (or (not b75) b78) b81))
(assert (or (or b81 (not b86)) b220))
(assert (or (or (not b81) b83) b86))
(assert (or (not b59) b198))
(assert (or (or (not b58) b59) b202))
(assert (or (or b56 b58) (not b59)))
(assert (or (or b58 (not b64)) b205))
(assert (or (or (not b58) b62) b64))
(assert (or (or b64 (not b69)) b208))
(assert (or (or (not b64) b67) b69))
(assert (or (not b43) b186))
(assert (or (or (not b42) b43) b189))
(assert (or (or b40 b42) (not b43)))
(assert (or (or b42 (not b48)) b192))
(assert (or (or (not b42) b46) b48))
(assert (or (or b48 (not b53)) b195))
(assert (or (or (not b48) b51) b53))
(assert (or b14 b17))
(assert (or (or b17 (not b23)) b174))
(assert (or (or (not b17) b20) b23))
(assert (or (or b23 (not b29)) b177))
(assert (or (or (not b23) b26) b29))
(assert (or (or b29 (not b35)) b180))
(assert (or (or (not b29) b32) b35))
(assert (or b35 b183))
(assert (or b126 (not b128)))
(assert (or (or b128 b131) (not b133)))
(assert (or (or (or (or (not b128) b133) b247) b259) b271))
(assert (or (or (or (or b133 b136) (not b138)) b151) b161))
(assert (or (or (or (or (not b133) b138) b250) b262) b274))
(assert (or (or (or (or b138 b141) (not b143)) b156) b166))
(assert (or (or (or (or (not b138) b143) b253) b265) b277))
(assert (or (or (or b143 b146) (not b148)) b170))
(assert (or (or (or (or (not b143) b148) b256) b268) b280))
(assert (or b89 (not b91)))
(assert (or (or b91 b95) (not b97)))
(assert (or (or (or (or (not b91) b97) b211) b223) b235))
(assert (or (or (or (or b72 (not b74)) b97) b101) b113))
(assert (or (or (or (or b74 (not b97)) b214) b226) b238))
(assert (or (or (or (or b74 b78) (not b80)) b105) b118))
(assert (or (or (or (or (not b74) b80) b217) b229) b241))
(assert (or (or (or (or b80 b83) (not b85)) b109) b122))
(assert (or (or (or (or (not b80) b85) b220) b232) b244))
(assert (or b14 (not b16)))
(assert (or (or b16 b20) (not b22)))
(assert (or (or (or (or (not b16) b22) b174) b186) b198))
(assert (or (or (or (or b22 b26) (not b28)) b40) b56))
(assert (or (or (or (or (not b22) b28) b177) b189) b202))
(assert (or (or (or (or b28 b32) (not b34)) b46) b62))
(assert (or (or (or (or (not b28) b34) b180) b192) b205))
(assert (or (or (or b34 (not b38)) b51) b67))
(assert (or (or (or (or (not b34) b38) b183) b195) b208))
(assert (or b653 (= (- (- (- (- (- r84 r11) r209) r197) r140) r128) 0)))
(assert (or (or (or b633 b648) b656) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r87 r84) r211) r199) r187) r176) r166) r152) r142) r130) r118) r107) r97) r83) 0)))
(assert (or (or (or b636 b649) b657) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r90 r87) r213) r201) r189) r178) r168) r155) r144) r132) r120) r109) r99) r86) 0)))
(assert (or (or (or b639 b650) b658) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r93 r90) r215) r203) r191) r180) r170) r158) r146) r134) r122) r111) r101) r89) 0)))
(assert (or (or (or b642 b651) b659) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r116 r93) r217) r205) r193) r182) r172) r161) r148) r136) r124) r113) r103) r92) 0)))
(assert (or (or (or b645 b652) b660) (= (- (- (- (- (- (- (- (- (- (- (- (- (- r221 r116) r219) r207) r195) r184) r174) r164) r150) r138) r126) r115) r105) r95) 0)))
(assert (or (not b20) (not b174)))
(assert (or (not b26) (not b177)))
(assert (or (not b32) (not b180)))
(assert (or (not b20) (not b198)))
(assert (or (not b26) (not b202)))
(assert (or (not b32) (not b205)))
(assert (or (not b20) (not b186)))
(assert (or (not b26) (not b189)))
(assert (or (not b32) (not b192)))
(assert (or (not b14) (not b609)))
(assert (or (not b20) (not b614)))
(assert (or (not b26) (not b619)))
(assert (or (not b32) (not b624)))
(assert (or (not b14) (not b577)))
(assert (or (not b20) (not b582)))
(assert (or (not b26) (not b587)))
(assert (or (not b32) (not b592)))
(assert (or (not b14) (not b540)))
(assert (or (not b20) (not b546)))
(assert (or (not b26) (not b552)))
(assert (or (not b32) (not b558)))
(assert (or (not b14) (not b513)))
(assert (or (not b20) (not b518)))
(assert (or (not b26) (not b523)))
(assert (or (not b32) (not b528)))
(assert (or (not b14) (not b487)))
(assert (or (not b20) (not b493)))
(assert (or (not b26) (not b499)))
(assert (or (not b32) (not b505)))
(assert (or (not b14) (not b457)))
(assert (or (not b20) (not b464)))
(assert (or (not b26) (not b471)))
(assert (or (not b32) (not b478)))
(assert (or (not b40) (not b189)))
(assert (or (not b46) (not b192)))
(assert (or (not b51) (not b195)))
(assert (or (not b40) (not b202)))
(assert (or (not b46) (not b205)))
(assert (or (not b51) (not b208)))
(assert (or (not b40) (not b177)))
(assert (or (not b46) (not b180)))
(assert (or (not b51) (not b183)))
(assert (or (not b40) (not b619)))
(assert (or (not b46) (not b624)))
(assert (or (not b51) (not b629)))
(assert (or (not b40) (not b587)))
(assert (or (not b46) (not b592)))
(assert (or (not b51) (not b597)))
(assert (or (not b40) (not b552)))
(assert (or (not b46) (not b558)))
(assert (or (not b51) (not b564)))
(assert (or (not b40) (not b523)))
(assert (or (not b46) (not b528)))
(assert (or (not b51) (not b533)))
(assert (or (not b40) (not b499)))
(assert (or (not b46) (not b505)))
(assert (or (not b40) (not b471)))
(assert (or (not b46) (not b478)))
(assert (or (not b56) (not b202)))
(assert (or (not b62) (not b205)))
(assert (or (not b67) (not b208)))
(assert (or (not b56) (not b189)))
(assert (or (not b62) (not b192)))
(assert (or (not b67) (not b195)))
(assert (or (not b56) (not b177)))
(assert (or (not b62) (not b180)))
(assert (or (not b67) (not b183)))
(assert (or (not b56) (not b619)))
(assert (or (not b62) (not b624)))
(assert (or (not b67) (not b629)))
(assert (or (not b56) (not b587)))
(assert (or (not b62) (not b592)))
(assert (or (not b67) (not b597)))
(assert (or (not b56) (not b552)))
(assert (or (not b62) (not b558)))
(assert (or (not b67) (not b564)))
(assert (or (not b56) (not b523)))
(assert (or (not b62) (not b528)))
(assert (or (not b67) (not b533)))
(assert (or (not b56) (not b499)))
(assert (or (not b62) (not b505)))
(assert (or (not b56) (not b471)))
(assert (or (not b62) (not b478)))
(assert (or (not b72) (not b214)))
(assert (or (not b78) (not b217)))
(assert (or (not b83) (not b220)))
(assert (or (not b72) (not b238)))
(assert (or (not b78) (not b241)))
(assert (or (not b83) (not b244)))
(assert (or (not b72) (not b226)))
(assert (or (not b78) (not b229)))
(assert (or (not b83) (not b232)))
(assert (or (not b72) (not b619)))
(assert (or (not b78) (not b624)))
(assert (or (not b83) (not b629)))
(assert (or (not b72) (not b587)))
(assert (or (not b78) (not b592)))
(assert (or (not b83) (not b597)))
(assert (or (not b72) (not b552)))
(assert (or (not b78) (not b558)))
(assert (or (not b83) (not b564)))
(assert (or (not b72) (not b523)))
(assert (or (not b78) (not b528)))
(assert (or (not b83) (not b533)))
(assert (or (not b72) (not b499)))
(assert (or (not b78) (not b505)))
(assert (or (not b72) (not b471)))
(assert (or (not b78) (not b478)))
(assert (or (not b95) (not b223)))
(assert (or (not b101) (not b226)))
(assert (or (not b105) (not b229)))
(assert (or (not b109) (not b232)))
(assert (or (not b95) (not b235)))
(assert (or (not b101) (not b238)))
(assert (or (not b105) (not b241)))
(assert (or (not b109) (not b244)))
(assert (or (not b95) (not b211)))
(assert (or (not b101) (not b214)))
(assert (or (not b105) (not b217)))
(assert (or (not b109) (not b220)))
(assert (or (not b89) (not b609)))
(assert (or (not b95) (not b614)))
(assert (or (not b101) (not b619)))
(assert (or (not b105) (not b624)))
(assert (or (not b109) (not b629)))
(assert (or (not b89) (not b577)))
(assert (or (not b95) (not b582)))
(assert (or (not b101) (not b587)))
(assert (or (not b105) (not b592)))
(assert (or (not b109) (not b597)))
(assert (or (not b89) (not b540)))
(assert (or (not b95) (not b546)))
(assert (or (not b101) (not b552)))
(assert (or (not b105) (not b558)))
(assert (or (not b109) (not b564)))
(assert (or (not b89) (not b513)))
(assert (or (not b95) (not b518)))
(assert (or (not b101) (not b523)))
(assert (or (not b105) (not b528)))
(assert (or (not b109) (not b533)))
(assert (or (not b89) (not b487)))
(assert (or (not b95) (not b493)))
(assert (or (not b101) (not b499)))
(assert (or (not b105) (not b505)))
(assert (or (not b89) (not b457)))
(assert (or (not b95) (not b464)))
(assert (or (not b101) (not b471)))
(assert (or (not b105) (not b478)))
(assert (or (not b113) (not b238)))
(assert (or (not b118) (not b241)))
(assert (or (not b122) (not b244)))
(assert (or (not b113) (not b226)))
(assert (or (not b118) (not b229)))
(assert (or (not b122) (not b232)))
(assert (or (not b113) (not b214)))
(assert (or (not b118) (not b217)))
(assert (or (not b122) (not b220)))
(assert (or (not b113) (not b619)))
(assert (or (not b118) (not b624)))
(assert (or (not b122) (not b629)))
(assert (or (not b113) (not b587)))
(assert (or (not b118) (not b592)))
(assert (or (not b122) (not b597)))
(assert (or (not b113) (not b552)))
(assert (or (not b118) (not b558)))
(assert (or (not b122) (not b564)))
(assert (or (not b113) (not b523)))
(assert (or (not b118) (not b528)))
(assert (or (not b122) (not b533)))
(assert (or (not b113) (not b499)))
(assert (or (not b118) (not b505)))
(assert (or (not b113) (not b471)))
(assert (or (not b118) (not b478)))
(assert (or (not b131) (not b247)))
(assert (or (not b136) (not b250)))
(assert (or (not b141) (not b253)))
(assert (or (not b146) (not b256)))
(assert (or (not b131) (not b271)))
(assert (or (not b136) (not b274)))
(assert (or (not b141) (not b277)))
(assert (or (not b146) (not b280)))
(assert (or (not b131) (not b259)))
(assert (or (not b136) (not b262)))
(assert (or (not b141) (not b265)))
(assert (or (not b146) (not b268)))
(assert (or (not b126) (not b609)))
(assert (or (not b131) (not b614)))
(assert (or (not b136) (not b619)))
(assert (or (not b141) (not b624)))
(assert (or (not b146) (not b629)))
(assert (or (not b126) (not b577)))
(assert (or (not b131) (not b582)))
(assert (or (not b136) (not b587)))
(assert (or (not b141) (not b592)))
(assert (or (not b146) (not b597)))
(assert (or (not b126) (not b540)))
(assert (or (not b131) (not b546)))
(assert (or (not b136) (not b552)))
(assert (or (not b141) (not b558)))
(assert (or (not b146) (not b564)))
(assert (or (not b126) (not b513)))
(assert (or (not b131) (not b518)))
(assert (or (not b136) (not b523)))
(assert (or (not b141) (not b528)))
(assert (or (not b146) (not b533)))
(assert (or (not b126) (not b487)))
(assert (or (not b131) (not b493)))
(assert (or (not b136) (not b499)))
(assert (or (not b141) (not b505)))
(assert (or (not b126) (not b457)))
(assert (or (not b131) (not b464)))
(assert (or (not b136) (not b471)))
(assert (or (not b141) (not b478)))
(assert (or (not b151) (not b262)))
(assert (or (not b156) (not b265)))
(assert (or (not b151) (not b274)))
(assert (or (not b156) (not b277)))
(assert (or (not b151) (not b250)))
(assert (or (not b156) (not b253)))
(assert (or (not b151) (not b619)))
(assert (or (not b156) (not b624)))
(assert (or (not b151) (not b587)))
(assert (or (not b156) (not b592)))
(assert (or (not b151) (not b552)))
(assert (or (not b156) (not b558)))
(assert (or (not b151) (not b523)))
(assert (or (not b156) (not b528)))
(assert (or (not b151) (not b499)))
(assert (or (not b156) (not b505)))
(assert (or (not b151) (not b471)))
(assert (or (not b156) (not b478)))
(assert (or (not b161) (not b274)))
(assert (or (not b166) (not b277)))
(assert (or (not b170) (not b280)))
(assert (or (not b161) (not b262)))
(assert (or (not b166) (not b265)))
(assert (or (not b170) (not b268)))
(assert (or (not b161) (not b250)))
(assert (or (not b166) (not b253)))
(assert (or (not b170) (not b256)))
(assert (or (not b161) (not b619)))
(assert (or (not b166) (not b624)))
(assert (or (not b170) (not b629)))
(assert (or (not b161) (not b587)))
(assert (or (not b166) (not b592)))
(assert (or (not b170) (not b597)))
(assert (or (not b161) (not b552)))
(assert (or (not b166) (not b558)))
(assert (or (not b170) (not b564)))
(assert (or (not b161) (not b523)))
(assert (or (not b166) (not b528)))
(assert (or (not b170) (not b533)))
(assert (or (not b161) (not b499)))
(assert (or (not b166) (not b505)))
(assert (or (not b161) (not b471)))
(assert (or (not b166) (not b478)))
(assert (or (not b174) (not b198)))
(assert (or (not b177) (not b202)))
(assert (or (not b180) (not b205)))
(assert (or (not b183) (not b208)))
(assert (or (not b174) (not b186)))
(assert (or (not b177) (not b189)))
(assert (or (not b180) (not b192)))
(assert (or (not b183) (not b195)))
(assert (or (not b174) (not b614)))
(assert (or (not b177) (not b619)))
(assert (or (not b180) (not b624)))
(assert (or (not b183) (not b629)))
(assert (or (not b174) (not b582)))
(assert (or (not b177) (not b587)))
(assert (or (not b180) (not b592)))
(assert (or (not b183) (not b597)))
(assert (or (not b174) (not b546)))
(assert (or (not b177) (not b552)))
(assert (or (not b180) (not b558)))
(assert (or (not b183) (not b564)))
(assert (or (not b174) (not b518)))
(assert (or (not b177) (not b523)))
(assert (or (not b180) (not b528)))
(assert (or (not b183) (not b533)))
(assert (or (not b174) (not b493)))
(assert (or (not b177) (not b499)))
(assert (or (not b180) (not b505)))
(assert (or (not b174) (not b464)))
(assert (or (not b177) (not b471)))
(assert (or (not b180) (not b478)))
(assert (or (not b186) (not b198)))
(assert (or (not b189) (not b202)))
(assert (or (not b192) (not b205)))
(assert (or (not b195) (not b208)))
(assert (or (not b186) (not b614)))
(assert (or (not b189) (not b619)))
(assert (or (not b192) (not b624)))
(assert (or (not b195) (not b629)))
(assert (or (not b186) (not b582)))
(assert (or (not b189) (not b587)))
(assert (or (not b192) (not b592)))
(assert (or (not b195) (not b597)))
(assert (or (not b186) (not b546)))
(assert (or (not b189) (not b552)))
(assert (or (not b192) (not b558)))
(assert (or (not b195) (not b564)))
(assert (or (not b186) (not b518)))
(assert (or (not b189) (not b523)))
(assert (or (not b192) (not b528)))
(assert (or (not b195) (not b533)))
(assert (or (not b186) (not b493)))
(assert (or (not b189) (not b499)))
(assert (or (not b192) (not b505)))
(assert (or (not b186) (not b464)))
(assert (or (not b189) (not b471)))
(assert (or (not b192) (not b478)))
(assert (or (not b198) (not b614)))
(assert (or (not b202) (not b619)))
(assert (or (not b205) (not b624)))
(assert (or (not b208) (not b629)))
(assert (or (not b198) (not b582)))
(assert (or (not b202) (not b587)))
(assert (or (not b205) (not b592)))
(assert (or (not b208) (not b597)))
(assert (or (not b198) (not b546)))
(assert (or (not b202) (not b552)))
(assert (or (not b205) (not b558)))
(assert (or (not b208) (not b564)))
(assert (or (not b198) (not b518)))
(assert (or (not b202) (not b523)))
(assert (or (not b205) (not b528)))
(assert (or (not b208) (not b533)))
(assert (or (not b198) (not b493)))
(assert (or (not b202) (not b499)))
(assert (or (not b205) (not b505)))
(assert (or (not b198) (not b464)))
(assert (or (not b202) (not b471)))
(assert (or (not b205) (not b478)))
(assert (or (not b211) (not b235)))
(assert (or (not b214) (not b238)))
(assert (or (not b217) (not b241)))
(assert (or (not b220) (not b244)))
(assert (or (not b211) (not b223)))
(assert (or (not b214) (not b226)))
(assert (or (not b217) (not b229)))
(assert (or (not b220) (not b232)))
(assert (or (not b211) (not b614)))
(assert (or (not b214) (not b619)))
(assert (or (not b217) (not b624)))
(assert (or (not b220) (not b629)))
(assert (or (not b211) (not b582)))
(assert (or (not b214) (not b587)))
(assert (or (not b217) (not b592)))
(assert (or (not b220) (not b597)))
(assert (or (not b211) (not b546)))
(assert (or (not b214) (not b552)))
(assert (or (not b217) (not b558)))
(assert (or (not b220) (not b564)))
(assert (or (not b211) (not b518)))
(assert (or (not b214) (not b523)))
(assert (or (not b217) (not b528)))
(assert (or (not b220) (not b533)))
(assert (or (not b211) (not b493)))
(assert (or (not b214) (not b499)))
(assert (or (not b217) (not b505)))
(assert (or (not b211) (not b464)))
(assert (or (not b214) (not b471)))
(assert (or (not b217) (not b478)))
(assert (or (not b223) (not b235)))
(assert (or (not b226) (not b238)))
(assert (or (not b229) (not b241)))
(assert (or (not b232) (not b244)))
(assert (or (not b223) (not b614)))
(assert (or (not b226) (not b619)))
(assert (or (not b229) (not b624)))
(assert (or (not b232) (not b629)))
(assert (or (not b223) (not b582)))
(assert (or (not b226) (not b587)))
(assert (or (not b229) (not b592)))
(assert (or (not b232) (not b597)))
(assert (or (not b223) (not b546)))
(assert (or (not b226) (not b552)))
(assert (or (not b229) (not b558)))
(assert (or (not b232) (not b564)))
(assert (or (not b223) (not b518)))
(assert (or (not b226) (not b523)))
(assert (or (not b229) (not b528)))
(assert (or (not b232) (not b533)))
(assert (or (not b223) (not b493)))
(assert (or (not b226) (not b499)))
(assert (or (not b229) (not b505)))
(assert (or (not b223) (not b464)))
(assert (or (not b226) (not b471)))
(assert (or (not b229) (not b478)))
(assert (or (not b235) (not b614)))
(assert (or (not b238) (not b619)))
(assert (or (not b241) (not b624)))
(assert (or (not b244) (not b629)))
(assert (or (not b235) (not b582)))
(assert (or (not b238) (not b587)))
(assert (or (not b241) (not b592)))
(assert (or (not b244) (not b597)))
(assert (or (not b235) (not b546)))
(assert (or (not b238) (not b552)))
(assert (or (not b241) (not b558)))
(assert (or (not b244) (not b564)))
(assert (or (not b235) (not b518)))
(assert (or (not b238) (not b523)))
(assert (or (not b241) (not b528)))
(assert (or (not b244) (not b533)))
(assert (or (not b235) (not b493)))
(assert (or (not b238) (not b499)))
(assert (or (not b241) (not b505)))
(assert (or (not b235) (not b464)))
(assert (or (not b238) (not b471)))
(assert (or (not b241) (not b478)))
(assert (or (not b247) (not b271)))
(assert (or (not b250) (not b274)))
(assert (or (not b253) (not b277)))
(assert (or (not b256) (not b280)))
(assert (or (not b247) (not b259)))
(assert (or (not b250) (not b262)))
(assert (or (not b253) (not b265)))
(assert (or (not b256) (not b268)))
(assert (or (not b247) (not b614)))
(assert (or (not b250) (not b619)))
(assert (or (not b253) (not b624)))
(assert (or (not b256) (not b629)))
(assert (or (not b247) (not b582)))
(assert (or (not b250) (not b587)))
(assert (or (not b253) (not b592)))
(assert (or (not b256) (not b597)))
(assert (or (not b247) (not b546)))
(assert (or (not b250) (not b552)))
(assert (or (not b253) (not b558)))
(assert (or (not b256) (not b564)))
(assert (or (not b247) (not b518)))
(assert (or (not b250) (not b523)))
(assert (or (not b253) (not b528)))
(assert (or (not b256) (not b533)))
(assert (or (not b247) (not b493)))
(assert (or (not b250) (not b499)))
(assert (or (not b253) (not b505)))
(assert (or (not b247) (not b464)))
(assert (or (not b250) (not b471)))
(assert (or (not b253) (not b478)))
(assert (or (not b259) (not b271)))
(assert (or (not b262) (not b274)))
(assert (or (not b265) (not b277)))
(assert (or (not b268) (not b280)))
(assert (or (not b259) (not b614)))
(assert (or (not b262) (not b619)))
(assert (or (not b265) (not b624)))
(assert (or (not b268) (not b629)))
(assert (or (not b259) (not b582)))
(assert (or (not b262) (not b587)))
(assert (or (not b265) (not b592)))
(assert (or (not b268) (not b597)))
(assert (or (not b259) (not b546)))
(assert (or (not b262) (not b552)))
(assert (or (not b265) (not b558)))
(assert (or (not b268) (not b564)))
(assert (or (not b259) (not b518)))
(assert (or (not b262) (not b523)))
(assert (or (not b265) (not b528)))
(assert (or (not b268) (not b533)))
(assert (or (not b259) (not b493)))
(assert (or (not b262) (not b499)))
(assert (or (not b265) (not b505)))
(assert (or (not b259) (not b464)))
(assert (or (not b262) (not b471)))
(assert (or (not b265) (not b478)))
(assert (or (not b271) (not b614)))
(assert (or (not b274) (not b619)))
(assert (or (not b277) (not b624)))
(assert (or (not b280) (not b629)))
(assert (or (not b271) (not b582)))
(assert (or (not b274) (not b587)))
(assert (or (not b277) (not b592)))
(assert (or (not b280) (not b597)))
(assert (or (not b271) (not b546)))
(assert (or (not b274) (not b552)))
(assert (or (not b277) (not b558)))
(assert (or (not b280) (not b564)))
(assert (or (not b271) (not b518)))
(assert (or (not b274) (not b523)))
(assert (or (not b277) (not b528)))
(assert (or (not b280) (not b533)))
(assert (or (not b271) (not b493)))
(assert (or (not b274) (not b499)))
(assert (or (not b277) (not b505)))
(assert (or (not b271) (not b464)))
(assert (or (not b274) (not b471)))
(assert (or (not b277) (not b478)))
(assert (or (not b283) (not b633)))
(assert (or (not b289) (not b636)))
(assert (or (not b295) (not b639)))
(assert (or (not b301) (not b642)))
(assert (or (not b283) (not b487)))
(assert (or (not b289) (not b493)))
(assert (or (not b295) (not b499)))
(assert (or (not b301) (not b505)))
(assert (or (not b283) (not b457)))
(assert (or (not b289) (not b464)))
(assert (or (not b295) (not b471)))
(assert (or (not b301) (not b478)))
(assert (or (not b283) (not b310)))
(assert (or (not b289) (not b316)))
(assert (or (not b295) (not b322)))
(assert (or (not b301) (not b328)))
(assert (or (not b247) (not b289)))
(assert (or (not b250) (not b295)))
(assert (or (not b253) (not b301)))
(assert (or (not b211) (not b289)))
(assert (or (not b214) (not b295)))
(assert (or (not b217) (not b301)))
(assert (or (not b174) (not b289)))
(assert (or (not b177) (not b295)))
(assert (or (not b180) (not b301)))
(assert (or (not b126) (not b283)))
(assert (or (not b131) (not b289)))
(assert (or (not b136) (not b295)))
(assert (or (not b141) (not b301)))
(assert (or (not b72) (not b295)))
(assert (or (not b78) (not b301)))
(assert (or (not b14) (not b283)))
(assert (or (not b20) (not b289)))
(assert (or (not b26) (not b295)))
(assert (or (not b32) (not b301)))
(assert (or (not b283) (not b577)))
(assert (or (not b289) (not b582)))
(assert (or (not b295) (not b587)))
(assert (or (not b301) (not b592)))
(assert (or (not b283) (not b513)))
(assert (or (not b289) (not b518)))
(assert (or (not b295) (not b523)))
(assert (or (not b301) (not b528)))
(assert (or (not b283) (not b400)))
(assert (or (not b289) (not b405)))
(assert (or (not b295) (not b410)))
(assert (or (not b301) (not b415)))
(assert (or (not b283) (not b337)))
(assert (or (not b289) (not b342)))
(assert (or (not b295) (not b347)))
(assert (or (not b301) (not b352)))
(assert (or (not b283) (not b648)))
(assert (or (not b289) (not b649)))
(assert (or (not b295) (not b650)))
(assert (or (not b301) (not b651)))
(assert (or (not b283) (not b540)))
(assert (or (not b289) (not b546)))
(assert (or (not b295) (not b552)))
(assert (or (not b301) (not b558)))
(assert (or (not b283) (not b363)))
(assert (or (not b289) (not b369)))
(assert (or (not b295) (not b375)))
(assert (or (not b301) (not b381)))
(assert (or (not b259) (not b289)))
(assert (or (not b262) (not b295)))
(assert (or (not b265) (not b301)))
(assert (or (not b223) (not b289)))
(assert (or (not b226) (not b295)))
(assert (or (not b229) (not b301)))
(assert (or (not b186) (not b289)))
(assert (or (not b189) (not b295)))
(assert (or (not b192) (not b301)))
(assert (or (not b151) (not b295)))
(assert (or (not b156) (not b301)))
(assert (or (not b89) (not b283)))
(assert (or (not b95) (not b289)))
(assert (or (not b101) (not b295)))
(assert (or (not b105) (not b301)))
(assert (or (not b40) (not b295)))
(assert (or (not b46) (not b301)))
(assert (or (not b283) (not b656)))
(assert (or (not b289) (not b657)))
(assert (or (not b295) (not b658)))
(assert (or (not b301) (not b659)))
(assert (or (not b283) (not b609)))
(assert (or (not b289) (not b614)))
(assert (or (not b295) (not b619)))
(assert (or (not b301) (not b624)))
(assert (or (not b283) (not b432)))
(assert (or (not b289) (not b437)))
(assert (or (not b295) (not b442)))
(assert (or (not b301) (not b447)))
(assert (or (not b310) (not b633)))
(assert (or (not b316) (not b636)))
(assert (or (not b322) (not b639)))
(assert (or (not b328) (not b642)))
(assert (or (not b310) (not b487)))
(assert (or (not b316) (not b493)))
(assert (or (not b322) (not b499)))
(assert (or (not b328) (not b505)))
(assert (or (not b310) (not b457)))
(assert (or (not b316) (not b464)))
(assert (or (not b322) (not b471)))
(assert (or (not b328) (not b478)))
(assert (or (not b247) (not b316)))
(assert (or (not b250) (not b322)))
(assert (or (not b253) (not b328)))
(assert (or (not b211) (not b316)))
(assert (or (not b214) (not b322)))
(assert (or (not b217) (not b328)))
(assert (or (not b174) (not b316)))
(assert (or (not b177) (not b322)))
(assert (or (not b180) (not b328)))
(assert (or (not b126) (not b310)))
(assert (or (not b131) (not b316)))
(assert (or (not b136) (not b322)))
(assert (or (not b141) (not b328)))
(assert (or (not b72) (not b322)))
(assert (or (not b78) (not b328)))
(assert (or (not b14) (not b310)))
(assert (or (not b20) (not b316)))
(assert (or (not b26) (not b322)))
(assert (or (not b32) (not b328)))
(assert (or (not b310) (not b577)))
(assert (or (not b316) (not b582)))
(assert (or (not b322) (not b587)))
(assert (or (not b328) (not b592)))
(assert (or (not b310) (not b513)))
(assert (or (not b316) (not b518)))
(assert (or (not b322) (not b523)))
(assert (or (not b328) (not b528)))
(assert (or (not b310) (not b400)))
(assert (or (not b316) (not b405)))
(assert (or (not b322) (not b410)))
(assert (or (not b328) (not b415)))
(assert (or (not b310) (not b337)))
(assert (or (not b316) (not b342)))
(assert (or (not b322) (not b347)))
(assert (or (not b328) (not b352)))
(assert (or (not b310) (not b656)))
(assert (or (not b316) (not b657)))
(assert (or (not b322) (not b658)))
(assert (or (not b328) (not b659)))
(assert (or (not b310) (not b609)))
(assert (or (not b316) (not b614)))
(assert (or (not b322) (not b619)))
(assert (or (not b328) (not b624)))
(assert (or (not b310) (not b432)))
(assert (or (not b316) (not b437)))
(assert (or (not b322) (not b442)))
(assert (or (not b328) (not b447)))
(assert (or (not b271) (not b316)))
(assert (or (not b274) (not b322)))
(assert (or (not b277) (not b328)))
(assert (or (not b235) (not b316)))
(assert (or (not b238) (not b322)))
(assert (or (not b241) (not b328)))
(assert (or (not b198) (not b316)))
(assert (or (not b202) (not b322)))
(assert (or (not b205) (not b328)))
(assert (or (not b161) (not b322)))
(assert (or (not b166) (not b328)))
(assert (or (not b113) (not b322)))
(assert (or (not b118) (not b328)))
(assert (or (not b56) (not b322)))
(assert (or (not b62) (not b328)))
(assert (or (not b310) (not b648)))
(assert (or (not b316) (not b649)))
(assert (or (not b322) (not b650)))
(assert (or (not b328) (not b651)))
(assert (or (not b310) (not b540)))
(assert (or (not b316) (not b546)))
(assert (or (not b322) (not b552)))
(assert (or (not b328) (not b558)))
(assert (or (not b310) (not b363)))
(assert (or (not b316) (not b369)))
(assert (or (not b322) (not b375)))
(assert (or (not b328) (not b381)))
(assert (or (not b337) (not b648)))
(assert (or (not b342) (not b649)))
(assert (or (not b347) (not b650)))
(assert (or (not b352) (not b651)))
(assert (or (not b357) (not b652)))
(assert (or (not b337) (not b540)))
(assert (or (not b342) (not b546)))
(assert (or (not b347) (not b552)))
(assert (or (not b352) (not b558)))
(assert (or (not b357) (not b564)))
(assert (or (not b337) (not b513)))
(assert (or (not b342) (not b518)))
(assert (or (not b347) (not b523)))
(assert (or (not b352) (not b528)))
(assert (or (not b357) (not b533)))
(assert (or (not b337) (not b363)))
(assert (or (not b342) (not b369)))
(assert (or (not b347) (not b375)))
(assert (or (not b352) (not b381)))
(assert (or (not b357) (not b387)))
(assert (or (not b259) (not b342)))
(assert (or (not b262) (not b347)))
(assert (or (not b265) (not b352)))
(assert (or (not b268) (not b357)))
(assert (or (not b223) (not b342)))
(assert (or (not b226) (not b347)))
(assert (or (not b229) (not b352)))
(assert (or (not b232) (not b357)))
(assert (or (not b186) (not b342)))
(assert (or (not b189) (not b347)))
(assert (or (not b192) (not b352)))
(assert (or (not b195) (not b357)))
(assert (or (not b151) (not b347)))
(assert (or (not b156) (not b352)))
(assert (or (not b89) (not b337)))
(assert (or (not b95) (not b342)))
(assert (or (not b101) (not b347)))
(assert (or (not b105) (not b352)))
(assert (or (not b109) (not b357)))
(assert (or (not b40) (not b347)))
(assert (or (not b46) (not b352)))
(assert (or (not b51) (not b357)))
(assert (or (not b337) (not b609)))
(assert (or (not b342) (not b614)))
(assert (or (not b347) (not b619)))
(assert (or (not b352) (not b624)))
(assert (or (not b357) (not b629)))
(assert (or (not b337) (not b457)))
(assert (or (not b342) (not b464)))
(assert (or (not b347) (not b471)))
(assert (or (not b352) (not b478)))
(assert (or (not b337) (not b432)))
(assert (or (not b342) (not b437)))
(assert (or (not b347) (not b442)))
(assert (or (not b352) (not b447)))
(assert (or (not b357) (not b452)))
(assert (or (not b337) (not b633)))
(assert (or (not b342) (not b636)))
(assert (or (not b347) (not b639)))
(assert (or (not b352) (not b642)))
(assert (or (not b357) (not b645)))
(assert (or (not b337) (not b487)))
(assert (or (not b342) (not b493)))
(assert (or (not b347) (not b499)))
(assert (or (not b352) (not b505)))
(assert (or (not b247) (not b342)))
(assert (or (not b250) (not b347)))
(assert (or (not b253) (not b352)))
(assert (or (not b256) (not b357)))
(assert (or (not b211) (not b342)))
(assert (or (not b214) (not b347)))
(assert (or (not b217) (not b352)))
(assert (or (not b220) (not b357)))
(assert (or (not b174) (not b342)))
(assert (or (not b177) (not b347)))
(assert (or (not b180) (not b352)))
(assert (or (not b183) (not b357)))
(assert (or (not b126) (not b337)))
(assert (or (not b131) (not b342)))
(assert (or (not b136) (not b347)))
(assert (or (not b141) (not b352)))
(assert (or (not b146) (not b357)))
(assert (or (not b72) (not b347)))
(assert (or (not b78) (not b352)))
(assert (or (not b83) (not b357)))
(assert (or (not b14) (not b337)))
(assert (or (not b20) (not b342)))
(assert (or (not b26) (not b347)))
(assert (or (not b32) (not b352)))
(assert (or (not b337) (not b656)))
(assert (or (not b342) (not b657)))
(assert (or (not b347) (not b658)))
(assert (or (not b352) (not b659)))
(assert (or (not b357) (not b660)))
(assert (or (not b337) (not b577)))
(assert (or (not b342) (not b582)))
(assert (or (not b347) (not b587)))
(assert (or (not b352) (not b592)))
(assert (or (not b357) (not b597)))
(assert (or (not b337) (not b400)))
(assert (or (not b342) (not b405)))
(assert (or (not b347) (not b410)))
(assert (or (not b352) (not b415)))
(assert (or (not b357) (not b420)))
(assert (or (not b363) (not b648)))
(assert (or (not b369) (not b649)))
(assert (or (not b375) (not b650)))
(assert (or (not b381) (not b651)))
(assert (or (not b387) (not b652)))
(assert (or (not b363) (not b540)))
(assert (or (not b369) (not b546)))
(assert (or (not b375) (not b552)))
(assert (or (not b381) (not b558)))
(assert (or (not b387) (not b564)))
(assert (or (not b363) (not b513)))
(assert (or (not b369) (not b518)))
(assert (or (not b375) (not b523)))
(assert (or (not b381) (not b528)))
(assert (or (not b387) (not b533)))
(assert (or (not b259) (not b369)))
(assert (or (not b262) (not b375)))
(assert (or (not b265) (not b381)))
(assert (or (not b268) (not b387)))
(assert (or (not b223) (not b369)))
(assert (or (not b226) (not b375)))
(assert (or (not b229) (not b381)))
(assert (or (not b232) (not b387)))
(assert (or (not b186) (not b369)))
(assert (or (not b189) (not b375)))
(assert (or (not b192) (not b381)))
(assert (or (not b195) (not b387)))
(assert (or (not b151) (not b375)))
(assert (or (not b156) (not b381)))
(assert (or (not b89) (not b363)))
(assert (or (not b95) (not b369)))
(assert (or (not b101) (not b375)))
(assert (or (not b105) (not b381)))
(assert (or (not b109) (not b387)))
(assert (or (not b40) (not b375)))
(assert (or (not b46) (not b381)))
(assert (or (not b51) (not b387)))
(assert (or (not b363) (not b609)))
(assert (or (not b369) (not b614)))
(assert (or (not b375) (not b619)))
(assert (or (not b381) (not b624)))
(assert (or (not b387) (not b629)))
(assert (or (not b363) (not b457)))
(assert (or (not b369) (not b464)))
(assert (or (not b375) (not b471)))
(assert (or (not b381) (not b478)))
(assert (or (not b363) (not b432)))
(assert (or (not b369) (not b437)))
(assert (or (not b375) (not b442)))
(assert (or (not b381) (not b447)))
(assert (or (not b387) (not b452)))
(assert (or (not b363) (not b656)))
(assert (or (not b369) (not b657)))
(assert (or (not b375) (not b658)))
(assert (or (not b381) (not b659)))
(assert (or (not b387) (not b660)))
(assert (or (not b363) (not b577)))
(assert (or (not b369) (not b582)))
(assert (or (not b375) (not b587)))
(assert (or (not b381) (not b592)))
(assert (or (not b387) (not b597)))
(assert (or (not b363) (not b400)))
(assert (or (not b369) (not b405)))
(assert (or (not b375) (not b410)))
(assert (or (not b381) (not b415)))
(assert (or (not b387) (not b420)))
(assert (or (not b271) (not b369)))
(assert (or (not b274) (not b375)))
(assert (or (not b277) (not b381)))
(assert (or (not b280) (not b387)))
(assert (or (not b235) (not b369)))
(assert (or (not b238) (not b375)))
(assert (or (not b241) (not b381)))
(assert (or (not b244) (not b387)))
(assert (or (not b198) (not b369)))
(assert (or (not b202) (not b375)))
(assert (or (not b205) (not b381)))
(assert (or (not b208) (not b387)))
(assert (or (not b161) (not b375)))
(assert (or (not b166) (not b381)))
(assert (or (not b170) (not b387)))
(assert (or (not b113) (not b375)))
(assert (or (not b118) (not b381)))
(assert (or (not b122) (not b387)))
(assert (or (not b56) (not b375)))
(assert (or (not b62) (not b381)))
(assert (or (not b67) (not b387)))
(assert (or (not b363) (not b633)))
(assert (or (not b369) (not b636)))
(assert (or (not b375) (not b639)))
(assert (or (not b381) (not b642)))
(assert (or (not b387) (not b645)))
(assert (or (not b363) (not b487)))
(assert (or (not b369) (not b493)))
(assert (or (not b375) (not b499)))
(assert (or (not b381) (not b505)))
(assert (or (not b393) (not b653)))
(assert (or (not b400) (not b656)))
(assert (or (not b405) (not b657)))
(assert (or (not b410) (not b658)))
(assert (or (not b415) (not b659)))
(assert (or (not b420) (not b660)))
(assert (or (not b393) (not b603)))
(assert (or (not b400) (not b609)))
(assert (or (not b405) (not b614)))
(assert (or (not b410) (not b619)))
(assert (or (not b415) (not b624)))
(assert (or (not b420) (not b629)))
(assert (or (not b393) (not b570)))
(assert (or (not b400) (not b577)))
(assert (or (not b405) (not b582)))
(assert (or (not b410) (not b587)))
(assert (or (not b415) (not b592)))
(assert (or (not b420) (not b597)))
(assert (or (not b393) (not b426)))
(assert (or (not b400) (not b432)))
(assert (or (not b405) (not b437)))
(assert (or (not b410) (not b442)))
(assert (or (not b415) (not b447)))
(assert (or (not b420) (not b452)))
(assert (or (not b271) (not b405)))
(assert (or (not b274) (not b410)))
(assert (or (not b277) (not b415)))
(assert (or (not b280) (not b420)))
(assert (or (not b235) (not b405)))
(assert (or (not b238) (not b410)))
(assert (or (not b241) (not b415)))
(assert (or (not b244) (not b420)))
(assert (or (not b198) (not b405)))
(assert (or (not b202) (not b410)))
(assert (or (not b205) (not b415)))
(assert (or (not b208) (not b420)))
(assert (or (not b161) (not b410)))
(assert (or (not b166) (not b415)))
(assert (or (not b170) (not b420)))
(assert (or (not b113) (not b410)))
(assert (or (not b118) (not b415)))
(assert (or (not b122) (not b420)))
(assert (or (not b56) (not b410)))
(assert (or (not b62) (not b415)))
(assert (or (not b67) (not b420)))
(assert (or (not b400) (not b540)))
(assert (or (not b405) (not b546)))
(assert (or (not b410) (not b552)))
(assert (or (not b415) (not b558)))
(assert (or (not b420) (not b564)))
(assert (or (not b400) (not b487)))
(assert (or (not b405) (not b493)))
(assert (or (not b410) (not b499)))
(assert (or (not b415) (not b505)))
(assert (or (not b400) (not b633)))
(assert (or (not b405) (not b636)))
(assert (or (not b410) (not b639)))
(assert (or (not b415) (not b642)))
(assert (or (not b420) (not b645)))
(assert (or (not b400) (not b457)))
(assert (or (not b405) (not b464)))
(assert (or (not b410) (not b471)))
(assert (or (not b415) (not b478)))
(assert (or (not b247) (not b405)))
(assert (or (not b250) (not b410)))
(assert (or (not b253) (not b415)))
(assert (or (not b256) (not b420)))
(assert (or (not b211) (not b405)))
(assert (or (not b214) (not b410)))
(assert (or (not b217) (not b415)))
(assert (or (not b220) (not b420)))
(assert (or (not b174) (not b405)))
(assert (or (not b177) (not b410)))
(assert (or (not b180) (not b415)))
(assert (or (not b183) (not b420)))
(assert (or (not b126) (not b400)))
(assert (or (not b131) (not b405)))
(assert (or (not b136) (not b410)))
(assert (or (not b141) (not b415)))
(assert (or (not b146) (not b420)))
(assert (or (not b72) (not b410)))
(assert (or (not b78) (not b415)))
(assert (or (not b83) (not b420)))
(assert (or (not b14) (not b400)))
(assert (or (not b20) (not b405)))
(assert (or (not b26) (not b410)))
(assert (or (not b32) (not b415)))
(assert (or (not b400) (not b648)))
(assert (or (not b405) (not b649)))
(assert (or (not b410) (not b650)))
(assert (or (not b415) (not b651)))
(assert (or (not b420) (not b652)))
(assert (or (not b400) (not b513)))
(assert (or (not b405) (not b518)))
(assert (or (not b410) (not b523)))
(assert (or (not b415) (not b528)))
(assert (or (not b420) (not b533)))
(assert (or (not b426) (not b653)))
(assert (or (not b432) (not b656)))
(assert (or (not b437) (not b657)))
(assert (or (not b442) (not b658)))
(assert (or (not b447) (not b659)))
(assert (or (not b452) (not b660)))
(assert (or (not b426) (not b603)))
(assert (or (not b432) (not b609)))
(assert (or (not b437) (not b614)))
(assert (or (not b442) (not b619)))
(assert (or (not b447) (not b624)))
(assert (or (not b452) (not b629)))
(assert (or (not b426) (not b570)))
(assert (or (not b432) (not b577)))
(assert (or (not b437) (not b582)))
(assert (or (not b442) (not b587)))
(assert (or (not b447) (not b592)))
(assert (or (not b452) (not b597)))
(assert (or (not b271) (not b437)))
(assert (or (not b274) (not b442)))
(assert (or (not b277) (not b447)))
(assert (or (not b280) (not b452)))
(assert (or (not b235) (not b437)))
(assert (or (not b238) (not b442)))
(assert (or (not b241) (not b447)))
(assert (or (not b244) (not b452)))
(assert (or (not b198) (not b437)))
(assert (or (not b202) (not b442)))
(assert (or (not b205) (not b447)))
(assert (or (not b208) (not b452)))
(assert (or (not b161) (not b442)))
(assert (or (not b166) (not b447)))
(assert (or (not b170) (not b452)))
(assert (or (not b113) (not b442)))
(assert (or (not b118) (not b447)))
(assert (or (not b122) (not b452)))
(assert (or (not b56) (not b442)))
(assert (or (not b62) (not b447)))
(assert (or (not b67) (not b452)))
(assert (or (not b432) (not b540)))
(assert (or (not b437) (not b546)))
(assert (or (not b442) (not b552)))
(assert (or (not b447) (not b558)))
(assert (or (not b452) (not b564)))
(assert (or (not b432) (not b487)))
(assert (or (not b437) (not b493)))
(assert (or (not b442) (not b499)))
(assert (or (not b447) (not b505)))
(assert (or (not b432) (not b648)))
(assert (or (not b437) (not b649)))
(assert (or (not b442) (not b650)))
(assert (or (not b447) (not b651)))
(assert (or (not b452) (not b652)))
(assert (or (not b432) (not b513)))
(assert (or (not b437) (not b518)))
(assert (or (not b442) (not b523)))
(assert (or (not b447) (not b528)))
(assert (or (not b452) (not b533)))
(assert (or (not b259) (not b437)))
(assert (or (not b262) (not b442)))
(assert (or (not b265) (not b447)))
(assert (or (not b268) (not b452)))
(assert (or (not b223) (not b437)))
(assert (or (not b226) (not b442)))
(assert (or (not b229) (not b447)))
(assert (or (not b232) (not b452)))
(assert (or (not b186) (not b437)))
(assert (or (not b189) (not b442)))
(assert (or (not b192) (not b447)))
(assert (or (not b195) (not b452)))
(assert (or (not b151) (not b442)))
(assert (or (not b156) (not b447)))
(assert (or (not b89) (not b432)))
(assert (or (not b95) (not b437)))
(assert (or (not b101) (not b442)))
(assert (or (not b105) (not b447)))
(assert (or (not b109) (not b452)))
(assert (or (not b40) (not b442)))
(assert (or (not b46) (not b447)))
(assert (or (not b51) (not b452)))
(assert (or (not b432) (not b633)))
(assert (or (not b437) (not b636)))
(assert (or (not b442) (not b639)))
(assert (or (not b447) (not b642)))
(assert (or (not b452) (not b645)))
(assert (or (not b432) (not b457)))
(assert (or (not b437) (not b464)))
(assert (or (not b442) (not b471)))
(assert (or (not b447) (not b478)))
(assert (or (not b457) (not b633)))
(assert (or (not b464) (not b636)))
(assert (or (not b471) (not b639)))
(assert (or (not b478) (not b642)))
(assert (or (not b457) (not b487)))
(assert (or (not b464) (not b493)))
(assert (or (not b471) (not b499)))
(assert (or (not b478) (not b505)))
(assert (or (not b457) (not b577)))
(assert (or (not b464) (not b582)))
(assert (or (not b471) (not b587)))
(assert (or (not b478) (not b592)))
(assert (or (not b457) (not b513)))
(assert (or (not b464) (not b518)))
(assert (or (not b471) (not b523)))
(assert (or (not b478) (not b528)))
(assert (or (not b457) (not b648)))
(assert (or (not b464) (not b649)))
(assert (or (not b471) (not b650)))
(assert (or (not b478) (not b651)))
(assert (or (not b457) (not b540)))
(assert (or (not b464) (not b546)))
(assert (or (not b471) (not b552)))
(assert (or (not b478) (not b558)))
(assert (or (not b457) (not b656)))
(assert (or (not b464) (not b657)))
(assert (or (not b471) (not b658)))
(assert (or (not b478) (not b659)))
(assert (or (not b457) (not b609)))
(assert (or (not b464) (not b614)))
(assert (or (not b471) (not b619)))
(assert (or (not b478) (not b624)))
(assert (or (not b487) (not b633)))
(assert (or (not b493) (not b636)))
(assert (or (not b499) (not b639)))
(assert (or (not b505) (not b642)))
(assert (or (not b487) (not b577)))
(assert (or (not b493) (not b582)))
(assert (or (not b499) (not b587)))
(assert (or (not b505) (not b592)))
(assert (or (not b487) (not b513)))
(assert (or (not b493) (not b518)))
(assert (or (not b499) (not b523)))
(assert (or (not b505) (not b528)))
(assert (or (not b487) (not b656)))
(assert (or (not b493) (not b657)))
(assert (or (not b499) (not b658)))
(assert (or (not b505) (not b659)))
(assert (or (not b487) (not b609)))
(assert (or (not b493) (not b614)))
(assert (or (not b499) (not b619)))
(assert (or (not b505) (not b624)))
(assert (or (not b487) (not b648)))
(assert (or (not b493) (not b649)))
(assert (or (not b499) (not b650)))
(assert (or (not b505) (not b651)))
(assert (or (not b487) (not b540)))
(assert (or (not b493) (not b546)))
(assert (or (not b499) (not b552)))
(assert (or (not b505) (not b558)))
(assert (or (not b513) (not b648)))
(assert (or (not b518) (not b649)))
(assert (or (not b523) (not b650)))
(assert (or (not b528) (not b651)))
(assert (or (not b533) (not b652)))
(assert (or (not b513) (not b540)))
(assert (or (not b518) (not b546)))
(assert (or (not b523) (not b552)))
(assert (or (not b528) (not b558)))
(assert (or (not b533) (not b564)))
(assert (or (not b513) (not b609)))
(assert (or (not b518) (not b614)))
(assert (or (not b523) (not b619)))
(assert (or (not b528) (not b624)))
(assert (or (not b533) (not b629)))
(assert (or (not b513) (not b633)))
(assert (or (not b518) (not b636)))
(assert (or (not b523) (not b639)))
(assert (or (not b528) (not b642)))
(assert (or (not b533) (not b645)))
(assert (or (not b513) (not b656)))
(assert (or (not b518) (not b657)))
(assert (or (not b523) (not b658)))
(assert (or (not b528) (not b659)))
(assert (or (not b533) (not b660)))
(assert (or (not b513) (not b577)))
(assert (or (not b518) (not b582)))
(assert (or (not b523) (not b587)))
(assert (or (not b528) (not b592)))
(assert (or (not b533) (not b597)))
(assert (or (not b540) (not b648)))
(assert (or (not b546) (not b649)))
(assert (or (not b552) (not b650)))
(assert (or (not b558) (not b651)))
(assert (or (not b564) (not b652)))
(assert (or (not b540) (not b609)))
(assert (or (not b546) (not b614)))
(assert (or (not b552) (not b619)))
(assert (or (not b558) (not b624)))
(assert (or (not b564) (not b629)))
(assert (or (not b540) (not b656)))
(assert (or (not b546) (not b657)))
(assert (or (not b552) (not b658)))
(assert (or (not b558) (not b659)))
(assert (or (not b564) (not b660)))
(assert (or (not b540) (not b577)))
(assert (or (not b546) (not b582)))
(assert (or (not b552) (not b587)))
(assert (or (not b558) (not b592)))
(assert (or (not b564) (not b597)))
(assert (or (not b540) (not b633)))
(assert (or (not b546) (not b636)))
(assert (or (not b552) (not b639)))
(assert (or (not b558) (not b642)))
(assert (or (not b564) (not b645)))
(assert (or (not b570) (not b653)))
(assert (or (not b577) (not b656)))
(assert (or (not b582) (not b657)))
(assert (or (not b587) (not b658)))
(assert (or (not b592) (not b659)))
(assert (or (not b597) (not b660)))
(assert (or (not b570) (not b603)))
(assert (or (not b577) (not b609)))
(assert (or (not b582) (not b614)))
(assert (or (not b587) (not b619)))
(assert (or (not b592) (not b624)))
(assert (or (not b597) (not b629)))
(assert (or (not b577) (not b633)))
(assert (or (not b582) (not b636)))
(assert (or (not b587) (not b639)))
(assert (or (not b592) (not b642)))
(assert (or (not b597) (not b645)))
(assert (or (not b577) (not b648)))
(assert (or (not b582) (not b649)))
(assert (or (not b587) (not b650)))
(assert (or (not b592) (not b651)))
(assert (or (not b597) (not b652)))
(assert (or (not b603) (not b653)))
(assert (or (not b609) (not b656)))
(assert (or (not b614) (not b657)))
(assert (or (not b619) (not b658)))
(assert (or (not b624) (not b659)))
(assert (or (not b629) (not b660)))
(assert (or (not b609) (not b648)))
(assert (or (not b614) (not b649)))
(assert (or (not b619) (not b650)))
(assert (or (not b624) (not b651)))
(assert (or (not b629) (not b652)))
(assert (or (not b609) (not b633)))
(assert (or (not b614) (not b636)))
(assert (or (not b619) (not b639)))
(assert (or (not b624) (not b642)))
(assert (or (not b629) (not b645)))
(assert (or (not b633) (not b656)))
(assert (or (not b636) (not b657)))
(assert (or (not b639) (not b658)))
(assert (or (not b642) (not b659)))
(assert (or (not b645) (not b660)))
(assert (or (not b633) (not b648)))
(assert (or (not b636) (not b649)))
(assert (or (not b639) (not b650)))
(assert (or (not b642) (not b651)))
(assert (or (not b645) (not b652)))
(assert (or (not b648) (not b656)))
(assert (or (not b649) (not b657)))
(assert (or (not b650) (not b658)))
(assert (or (not b651) (not b659)))
(assert (or (not b652) (not b660)))
(assert (= r1 0))
(assert (= r2 r3))
(assert (= (- r4 r1) 1))
(assert (= (- r5 r4) 1))
(assert (= (- r6 r5) 1))
(assert (= (- r7 r6) 1))
(assert (= (- r8 r7) 1))
(assert (= (- r3 r8) 1))
(assert (= r9 0))
(assert (= r10 0))
(assert (= r11 1773))
(assert (<= (+ (* 1 r2) (* 1 r12)) 6787))
(assert (= r17 0))
(assert (= r42 0))
(assert (= r94 0))
(assert (= r95 0))
(assert (= r104 0))
(assert (= r105 0))
(assert (= r163 0))
(assert (= r164 0))
(assert (= r173 0))
(assert (= r174 0))
(assert (= (- r153 r10) 0))
(assert (= (- (- (- (- r156 r153) r35) r27) r13) 0))
(assert (= (- (- (- (- (- (- (- (- (- (- (- (- (- r159 r156) r78) r74) r70) r66) r62) r58) r54) r50) r46) r36) r28) r14) 0))
(assert (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r162 r159) r79) r75) r71) r67) r63) r59) r55) r51) r47) r43) r40) r37) r32) r29) r24) r21) r18) r15) 0))
(assert (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r185 r162) r80) r76) r72) r68) r64) r60) r56) r52) r48) r44) r41) r38) r33) r30) r25) r22) r19) r16) 0))
(assert (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- r222 r185) r81) r77) r73) r69) r65) r61) r57) r53) r49) r45) r42) r39) r34) r31) r26) r23) r20) r17) 0))
(assert (= (- (- (- (- (- r223 r9) r208) r196) r139) r127) 0))
(assert (= (- (- (- (- (- (- (- (- (- (- (- (- (- r224 r223) r210) r198) r186) r175) r165) r151) r141) r129) r117) r106) r96) r82) 0))
(assert (= (- (- (- (- (- (- (- (- (- (- (- (- (- r225 r224) r212) r200) r188) r177) r167) r154) r143) r131) r119) r108) r98) r85) 0))
(assert (= (- (- (- (- (- (- (- (- (- (- (- (- (- r226 r225) r214) r202) r190) r179) r169) r157) r145) r133) r121) r110) r100) r88) 0))
(assert (= (- (- (- (- (- (- (- (- (- (- (- (- (- r227 r226) r216) r204) r192) r181) r171) r160) r147) r135) r123) r112) r102) r91) 0))
(assert (= (- (- (- (- (- (- (- (- (- (- (- (- (- r12 r227) r218) r206) r194) r183) r173) r163) r149) r137) r125) r114) r104) r94) 0))
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
